Library hanoi.shanoi4

From mathcomp Require Import all_ssreflect finmap.
From hanoi Require Import extra star gdist lhanoi3 ghanoi ghanoi4 shanoi.

Open Scope nat_scope.

Set Implicit Arguments.
Unset Strict Implicit.


Section sHanoi4.

Local Notation "c1 `-->_s c2" := (smove c1 c2)
    (format "c1 `-->_s c2", at level 60).
Local Notation "c1 `-->*_s c2" := (connect smove c1 c2)
    (format "c1 `-->*_s c2", at level 60).

Let p0 : peg 4 := ord0.

Lemma pE4 (p1 p2 p3 : peg 4) p :
   p1 != p2 → p1 != p3 → p2 != p3 →
   p1 != p0 → p2 != p0 → p3 != p0 →
  [\/ p = p0, p = p1, p = p2 | p = p3].
Proof.
rewrite /p0.
by case: (peg4E p1) ⇒ ->; rewrite ?eqxx //;
   case: (peg4E p2) ⇒ ->; rewrite ?eqxx //;
   case: (peg4E p3) ⇒ ->; rewrite ?eqxx //;
   case: (peg4E p) ⇒ ->; rewrite ?eqxx // ⇒ *;
   try ((by apply: Or41) || (by apply: Or42) ||
        (by apply: Or43) || (by apply: Or44)).
Qed.


Section lift.

Variable p1 p2 p3 : peg 4.

Hypothesis p1Dp0 : p1 != p0.
Hypothesis p2Dp0 : p2 != p0.
Hypothesis p3Dp0 : p3 != p0.
Hypothesis p1Dp2 : p1 != p2.
Hypothesis p1Dp3 : p1 != p3.
Hypothesis p2Dp3 : p2 != p3.

Variable n m : nat.

Definition clmap (c : configuration 3 n) : configuration 4 n :=
 [ffun i ⇒
    if c i == 0 :> nat then p1
    else if c i == 1 :> nat then p0 else p2].

Definition clmerge (c : configuration 3 n) : configuration 4 (n + m) :=
  cmerge (clmap c) `c[p3].

Lemma on_top_clmerge x c : on_top x c → on_top (tlshift m x) (clmerge c).
Proof.
move⇒ /on_topP oH; apply/on_topP ⇒ d.
rewrite !ffunE tsplit_tlshift /=.
case: tsplitP ⇒ y; rewrite !ffunE ⇒ →.
  case: (_ == _) ⇒ [/eqP|]; first by rewrite (negPf p1Dp3).
  case: (_ == _) ⇒ /eqP; first by rewrite eq_sym (negPf p3Dp0).
  by rewrite (negPf p2Dp3).
case: eqP ⇒ [cxE0|cxD0].
  case: eqP ⇒ [cyE0 _| _].
    by rewrite leq_add2r oH //; apply: val_inj; rewrite /= cyE0.
  by case: (_ == _) ⇒ /eqP; rewrite (negPf p1Dp0, negPf p1Dp2).
case: eqP ⇒ [cxE1|cxD1].
  case: (_ == _) ⇒ [/eqP|]; first by rewrite eq_sym (negPf p1Dp0).
  case: eqP ⇒ [cyE1 _|_ /eqP].
    by rewrite leq_add2r oH //; apply: val_inj; rewrite /= cyE1.
  by rewrite eq_sym (negPf p2Dp0).
have cxE2 : c x = 2 :> nat by case: (c x) cxD0 cxD1 ⇒ [] [|[|[]]].
case: eqP ⇒ [_ /eqP|cyD0].
  by rewrite eq_sym (negPf p1Dp2).
case: eqP ⇒ [_ /eqP|cyD1 _].
  by rewrite (negPf p2Dp0).
have cyE2 : c y = 2 :> nat by case: (c y) cyD0 cyD1 ⇒ [] [|[|[]]].
by rewrite leq_add2r oH //; apply: val_inj; rewrite /= cyE2.
Qed.

Lemma move_clmerge c1 c2 : lmove c1 c2 → clmerge c1 `-->_s clmerge c2.
Proof.
move⇒ /moveP [d1 [H1d1 H2d1 H3d1 H4d1]].
apply/moveP; ∃ (tlshift m d1); split ⇒ //.
- move: H1d1; rewrite !ffunE tsplit_tlshift !ffunE.
  rewrite /lrel /= /srel /ghanoi.srel /=.
  case: (c1 d1) ⇒ [] [|[|[|]]] //=.
  - case: (c2 d1) ⇒ [] [|[|[|]]] //=.
    by rewrite p1Dp0 muln0.
  - case: (c2 d1) ⇒ [] [|[|[|]]] //= _ _ _.
      by rewrite eq_sym p1Dp0.
    by rewrite eq_sym p2Dp0.
  case: (c2 d1) ⇒ [] [|[|[|]]] //= _ _ _.
  by rewrite p2Dp0 muln0.
- move⇒ d2; rewrite !ffunE; case: tsplitP ⇒ j; rewrite !ffunE //.
  move⇒ d2E /eqP/val_eqP.
  rewrite /= d2E eqn_add2r ⇒ H.
  by rewrite (@H2d1 j).
- by apply: on_top_clmerge.
by apply: on_top_clmerge.
Qed.

Lemma path_clmerge c cs :
  path (move (@lrel 3)) c cs →
  path smove (clmerge c) [seq clmerge c | c <- cs].
Proof.
elim: cs c ⇒ //= c1 cs IH c2 /andP[mH pH].
by rewrite move_clmerge // IH.
Qed.

Lemma gdist_clmerge c1 c2 :
  `d[clmerge c1, clmerge c2]_smove ≤ `d[c1, c2]_(move (@lrel 3)).
Proof.
have /gpath_connect[pa1 pa1H] := move_lconnect3 c1 c2.
rewrite (gpath_dist pa1H) -(size_map clmerge).
apply: gdist_path_le; first by rewrite path_clmerge // (gpath_path pa1H).
by rewrite [LHS]last_map (gpath_last pa1H).
Qed.

End lift.


Lemma leq_shanoi4 p1 p2 n :
   p1 != p0 → p2 != p0 → p1 != p2 →
   `d[`c[p1, n],`c[p2, n]]_smove ≤ (S_[1] n).*2.
Proof.
elim/ltn_ind : n p1 p2 ⇒ [] [|n] IH p1 p2 p1Dp0 p2Dp0 p1Dp2.
  rewrite alphaS_small double0.
  rewrite (_ : `c[p1] = `c[p2]) ?gdist0 //.
  by apply/ffunP⇒ [] [].
rewrite S1E S1_bigmin -muln2 -bigminMr.
apply/bigmin_leqP ⇒ i iLn.
have iLn1 : i ≤ n.+1 by apply: leq_trans iLn _.
rewrite -{-5}(subnK iLn1).
rewrite eq_sym in p2Dp0.
have [p3 [[p3Dp2 p3Dp0 p3Dp1] _]] := peg4comp3 p1Dp0 p1Dp2 p2Dp0.
rewrite eq_sym in p2Dp0.
pose p1n := `c[p1, n.+1 - i].
pose p2n := `c[p2, n.+1 - i].
pose p3n := `c[p3, n.+1 - i].
pose p1i := `c[p1, i].
pose p2i := `c[p2, i].
pose p3i := `c[p3, i].
pose c1 := cmerge p1n p1i.
pose c2 := cmerge p1n p3i.
pose c3 := cmerge p2n p3i.
pose c4 := cmerge p2n p2i.
have <- : c1 = `c[p1].
  apply/ffunP ⇒ j; rewrite /c1 !ffunE.
  by case: tsplitP ⇒ k; rewrite !ffunE.
have <- : c4 = `c[p2].
  apply/ffunP ⇒ j; rewrite /c1 !ffunE.
  by case: tsplitP ⇒ k; rewrite !ffunE.
apply: leq_trans
   (_ : _ ≤ `d[c1, c2]_smove + `d[c2, c3]_smove + `d[c3, c4]_smove) _.
  apply: leq_trans (leq_add (gdist_triangular _ _ _ _) (leqnn _)).
  apply: gdist_triangular.
rewrite -addnn !mulnDl [X in _ ≤ X]addnAC !muln2.
repeat apply: leq_add; first 2 last.
- apply: leq_trans (gdist_merger _ _ _) _; first by apply: sirr.
    by apply: shanoi_connect.
  by rewrite -S1E; apply: IH.
- apply: leq_trans (gdist_merger _ _ _) _; first by apply: sirr.
    by apply: shanoi_connect.
  by rewrite -S1E; apply: IH ⇒ //; rewrite eq_sym.
rewrite div2K; last first.
  rewrite -subn1 oddB ?expn_gt0 // addbT.
  by rewrite odd_exp orbT.
have → : c2 = clmerge p1 p2 p3 _ `c[ord0].
  apply/ffunP⇒ x; rewrite !ffunE.
  by case: tsplitP ⇒ // j; rewrite !ffunE /=.
have → : c3 = clmerge p1 p2 p3 _ `c[inord 2].
  apply/ffunP⇒ x; rewrite !ffunE.
  by case: tsplitP ⇒ // j; rewrite !ffunE /= inordK.
apply: leq_trans (gdist_clmerge _ _ _ _ _ _ _ _ _) _ ⇒ //;
  try by rewrite eq_sym.
rewrite gdist_lhanoi3p /lrel /= inordK //=.
case: eqP⇒ [/val_eqP/=|]; first by rewrite inordK.
by rewrite muln1.
Qed.

Fixpoint distanceL n (l : seq (configuration 4 n)) : nat :=
  if l is a :: l1 then
    if l1 is b :: _ then `d[a, b]_smove + distanceL l1
    else 0
  else 0.

Notation " D[ l ] " := (distanceL l)
  (format " D[ l ]").

Definition apeg p1 p2 n : peg 4 := if odd n then p2 else p1.
Notation " a[ p1 , p2 ] " := (apeg p1 p2)
  (format " a[ p1 , p2 ]").

Lemma apeg32E a p1 p2 : a[p1, p2] (3 × a).-2 = a[p1, p2] a.
Proof.
case: a ⇒ // a.
rewrite /apeg -subn2 oddB; last by rewrite mulnS.
by rewrite odd_mul /=; case: odd.
Qed.

Lemma apeg0 p1 p2 : a[p1, p2] 0 = p1.
Proof. by []. Qed.

Lemma apegS p1 p2 n : a[p1, p2] n.+1 = a[p2, p1] n.
Proof. by rewrite /apeg /=; case: odd. Qed.

Lemma apegO p1 p2 n : a[p1, p2] n = a[p2, p1] (~~ (odd n)).
Proof. by rewrite /apeg /=; case: odd. Qed.

Lemma apeg_double p1 p2 n : a[p1, p2] (n.*2) = p1.
Proof. by rewrite apegO odd_double. Qed.

Lemma apeg_neq p1 p2 p3 n : p1 != p3 → p2 != p3 → a[p1, p2] n != p3.
Proof. by rewrite /apeg /=; case: odd; rewrite // eq_sym. Qed.

Lemma apeg_eqC p1 p2 n : (a[p1, p2] n == a[p2, p1] n) = (p1 == p2).
Proof. by rewrite /apeg /=; case: odd; rewrite // eq_sym. Qed.

Lemma apegD p1 p2 m n : a[p1, p2] (m + n) = a[ a[p1, p2] n, a[p2, p1] n] m.
Proof. by rewrite /apeg oddD; do 2 case: odd. Qed.

Lemma apegMr p1 p2 m n : odd m → a[p1, p2] (m × n) = a[p1, p2] n.
Proof. by rewrite /apeg; rewrite odd_mul ⇒ →. Qed.

Lemma codom_apeg (A : finType) (f : {ffun A → _}) p1 p2 n :
  (codom f \subset [:: a[p1, p2] n; a[p2, p1] n]) =
  (codom f \subset [:: p1; p2]).
Proof. by rewrite /apeg; case: odd; rewrite // codom_subC. Qed.

Lemma sgdist_pair n (p2 : peg 4) (u v : configuration 4 n.+1)
    (p1 := u ldisk) (p3 := v ldisk):
   {st : (configuration 4 n × configuration 4 n) |
    p1 != p2 → p1 != p3 → p2 != p3 →
    p1 != p0 → p2 != p0 → p3 != p0 →
     [/\ codom st.1 \subset [:: p2; p3], codom st.2 \subset [:: p1; p2] &
         `d[u, v]_smove = D[[:: ↓[u]; st.1; st.2; ↓[v]]].+2]}.
Proof.
case: eqP ⇒ [_|/eqP p1Dp2]; first by ∃ (↓[u], ↓[v]).
case: eqP ⇒ [_|/eqP p1Dp3]; first by ∃ (↓[u], ↓[v]).
case: eqP ⇒ [_|/eqP p2Dp3]; first by ∃ (↓[u], ↓[v]).
case: eqP ⇒ [_|/eqP p1Dp0]; first by ∃ (↓[u], ↓[v]).
case: eqP ⇒ [_|/eqP p2Dp0]; first by ∃ (↓[u], ↓[v]).
case: eqP ⇒ [_|/eqP p3Dp0]; first by ∃ (↓[u], ↓[v]).
have pE p : [\/ p = p0, p = p1, p = p2 | p = p3] by apply: pE4.
have [cs /= csH] := gpath_connect (shanoi_connect u v).
have vIcs : v \in cs.
  have := mem_last u cs; rewrite (gpath_last csH).
  rewrite inE; case: eqP ⇒ // vEu.
  by case/eqP : p1Dp3; rewrite /p3 vEu.
case: (@split_first _ cs (fun c ⇒ c ldisk != p1)) ⇒ [|[[sp cs1] cs2]].
  apply/negP⇒ /allP /(_ _ vIcs).
  rewrite /= -topredE /= negbK.
  by rewrite eq_sym (negPf p1Dp3).
case⇒ /allP spH spLE csE.
pose s := last u cs1.
have sMsp : s `-->_s sp.
  by have := gpath_path csH; rewrite csE cat_path ⇒ /and3P[].
have sLp1 : s ldisk = p1.
  move: (spH s); rewrite /s; case: (cs1) ⇒ //= c cs3 /(_ (mem_last _ _)).
  by rewrite -topredE negbK ⇒ /eqP.
have spLp0 : sp ldisk = p0.
  apply/eqP.
  have /(_ ldisk) := move_diskr sMsp.
  rewrite eq_sym sLp1 ⇒ /(_ spLE) /andP[].
  case: (_ =P p0) ⇒ // /val_eqP /=.
  have /eqP/val_eqP/= := p1Dp0.
  by case: (p1 : nat) ⇒ // k; case: (sp _ : nat).
have sCd : codom (↓[s]) \subset [:: p2; p3].
  apply/subsetP⇒ i; rewrite !inE ⇒ /codomP[j] →.
  case: (pE (↓[s] j)) ⇒ [||->|->]; rewrite ?eqxx ?orbT //.
    rewrite ffunE trshift_lift /=.
    move/eqP; rewrite -spLp0 -[_ == _]negbK; case/negP.
    apply: move_on_toplDr sMsp _ _; first by rewrite sLp1 spLp0.
    by rewrite /= /bump [n ≤ j]leqNgt ltn_ord add0n ltnW.
  rewrite ffunE trshift_lift /=.
  move/eqP; rewrite -sLp1 -[_ == _]negbK; case/negP.
  apply: move_on_toplDl sMsp _ _; first by rewrite sLp1 spLp0.
  by rewrite /= /bump [n ≤ j]leqNgt ltn_ord add0n.
have vIcs2 : v \in cs2.
  move: vIcs; rewrite csE !(inE, mem_cat) ⇒ /or3P[|/eqP vEs|] //.
    by move⇒ /spH; rewrite /= -topredE negbK eq_sym (negPf p1Dp3).
  by case/eqP : p3Dp0; rewrite /p3 vEs.
case: (@split_last _ (sp :: cs2) (fun c ⇒ c ldisk != p3)) ⇒
     [|/= [[t cs3] cs4]/=].
  apply/negP⇒ /allP /(_ _ (mem_head _ _)).
  by rewrite /= -topredE /= negbK spLp0 eq_sym (negPf p3Dp0).
case⇒ // tLE tH scs2E.
have vIcs4 : v \in cs4.
  have := gpath_last csH; rewrite csE scs2E !last_cat /=.
  case: (cs4) ⇒ /= [tEv|c1 cs5 <-]; last by apply: mem_last.
  by case/eqP: tLE; rewrite tEv.
  case: cs4 tH scs2E vIcs4 ⇒ // tp cs4 /allP tH scs2E vItpcs4.
have tMtp : t `-->_s tp.
  by have := gpath_path csH; rewrite csE scs2E !cat_path /= ⇒ /and5P[].
have tpLp3 : tp ldisk = p3.
  by move: (tH _ (mem_head _ _)); rewrite /= -topredE negbK ⇒ /eqP.
have tLp0 : t ldisk = p0.
  apply/eqP.
  have /(_ ldisk) := move_diskr tMtp.
  rewrite tpLp3 ⇒ /(_ tLE) /andP[].
  case: (_ =P p0) ⇒ // /val_eqP /=.
  have /eqP/val_eqP/= := p3Dp0.
  by case: (p3 : nat) ⇒ // k; case: (t _ : nat).
have tCd : codom (↓[t]) \subset [:: p1; p2].
  apply/subsetP⇒ i; rewrite !inE ⇒ /codomP[j] →.
  case: (pE (↓[t] j)) ⇒ [|->|->|]; rewrite ?eqxx ?orbT //.
    rewrite ffunE trshift_lift /=.
    move/eqP; rewrite -tLp0 -[_ == _]negbK; case/negP.
    apply: move_on_toplDl tMtp _ _; first by rewrite tpLp3 tLp0 eq_sym.
    by rewrite /= /bump [n ≤ j]leqNgt ltn_ord add0n.
  rewrite ffunE trshift_lift /=.
  move/eqP; rewrite -tpLp3 -[_ == _]negbK; case/negP.
  apply: move_on_toplDr tMtp _ _; first by rewrite tpLp3 tLp0 eq_sym.
  by rewrite /= /bump [n ≤ j]leqNgt ltn_ord add0n ltnW.
∃ (↓[s], ↓[t]); split ⇒ //=.
rewrite addn0.
move: csH; rewrite csE ⇒ csH.
rewrite (gdist_cat csH) -/s.
move: csH ⇒ /gpath_catr; rewrite -/s ⇒ csH.
rewrite gdist_cunlift_eq //; try apply: sirr; last by apply: shanoi_connect.
rewrite -!addnS.
congr (_ + _).
have ->: ↓[s] = ↓[sp].
  have sLDspL : s ldisk != sp ldisk by rewrite sLp1 spLp0.
  apply/ffunP ⇒ i; rewrite !ffunE.
  apply: move_disk1 sMsp sLDspL _.
  by apply/negP ⇒ /eqP/val_eqP /=; rewrite eqn_leq leqNgt ltn_ord.
rewrite (gdist_cons csH) addnS; congr (_).+1.
move: csH ⇒ /gpath_consr csH.
have ctEctp : ↓[t] = ↓[tp].
  have tLDtpL : t ldisk != tp ldisk by rewrite tLp0 tpLp3 eq_sym.
  apply/ffunP ⇒ i; rewrite !ffunE.
  apply: move_disk1 tMtp tLDtpL _.
  by apply/negP ⇒ /eqP/val_eqP /=; rewrite eqn_leq leqNgt ltn_ord.
case: cs3 scs2E ⇒ [[spEt cs2E]|c3 cs3 /= [spE cs2E]].
  move: csH; rewrite spEt cs2E ⇒ csH.
  rewrite gdist0 add0n (gdist_cons csH) ctEctp.
  move: csH ⇒ /gpath_consr csH.
  rewrite gdist_cunlift_eq //; try by apply: sirr.
  by apply: shanoi_connect.
move: csH; rewrite cs2E -cat_rcons ⇒ csH.
rewrite (gdist_cat csH) last_rcons.
rewrite gdist_cunlift_eq //; try apply: sirr; last 2 first.
- by apply: shanoi_connect.
- by rewrite tLp0.
congr (_ + _).
move: csH ⇒ /gpath_catr; rewrite last_rcons ⇒ csH.
rewrite (gdist_cons csH); congr (_).+1.
move: csH ⇒ /gpath_consr csH.
rewrite ctEctp gdist_cunlift_eq //; try apply: sirr.
by apply: shanoi_connect.
Qed.

Definition sgdist1 n (p2 : peg 4) (u v : configuration 4 n.+1) :=
 let: (exist (x, _) _) := sgdist_pair p2 u v in x.

Definition sgdist2 n (p2 : peg 4) (u v : configuration 4 n.+1) :=
 let: (exist (_, x) _) := sgdist_pair p2 u v in x.

Lemma sgdistE n (p2 : peg 4) (u v : configuration 4 n.+1)
    (p1 := u ldisk) (p3 := v ldisk):
    p1 != p2 → p1 != p3 → p2 != p3 →
    p1 != p0 → p2 != p0 → p3 != p0 →
   [/\ codom (sgdist1 p2 u v) \subset [:: p2; p3],
       codom (sgdist2 p2 u v) \subset [:: p1; p2] &
       `d[u, v]_smove = D[[:: ↓[u]; sgdist1 p2 u v; sgdist2 p2 u v; ↓[v]]].+2].
Proof.
move⇒ p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0.
by rewrite /sgdist1 /sgdist2; case: sgdist_pair ⇒ [] [x y] [].
Qed.

Definition beta n l k :=
  if ((1 < l) && (k == n.-1)) then α_[l] k else (α_[1] k).*2.

Local Notation "β_[ n , l ]" := (beta n l) (format "β_[ n , l ]" ).

Lemma leq_beta n l k : α_[l] k ≤ β_[n, l] k.
Proof.
rewrite /beta; case: (_ < _) ⇒ /=; last first.
  by apply: bound_alphaL.
by case: (_ == _) ⇒ //=; apply: bound_alphaL.
Qed.

Lemma geq_beta n l k : β_[n, l] k ≤ (α_[1] k).*2.
Proof.
rewrite /beta; case: (_ < _) ⇒ //=.
by case: (_ == _) ⇒ //=; apply: bound_alphaL.
Qed.

Lemma beta1E n k : β_[n, 1] k = (α_[1] k).*2.
Proof. by rewrite /beta ltnn. Qed.

Definition sp n (a : configuration 4 n) l p :=
  \sum_(k < n) (a k != p) × β_[n, l] k.

Lemma sum_beta_S n l (a : configuration 4 n.+1) p : 1 < l →
  sp a l p =
  \sum_(k < n) ((↓[a] k != p) × (α_[1] k).*2) + (a ord_max != p) × α_[l] n.
Proof.
move⇒ l_gt1; rewrite /sp.
rewrite big_ord_recr /= /beta l_gt1 eqxx /=; congr (_ + _).
apply: eq_bigr ⇒ i _; rewrite !ffunE; congr ((a _ != _) × _).
  by apply: val_inj.
by rewrite eqn_leq [_ ≤ i]leqNgt ltn_ord andbF.
Qed.

Lemma leq_sum_beta n l a :
  \sum_(k < n) a k × β_[n, l] k ≤ \sum_(k < n) a k × (α_[1] k).*2.
Proof.
by apply: leq_sum ⇒ i _; rewrite leq_mul2l geq_beta orbT.
Qed.

Lemma sum_alpha_diffE n (f : configuration 4 n.+1) (p1 p2 : peg 4) v1 v2 :
  1 < v1 → 1 < v2 → p1 != p2 → codom f \subset [:: p1; p2] →
  sp f v1 p1 + sp f v2 p2 ≤ (S_[1] n).*2 + α_[maxn v1 v2] n.
Proof.
move⇒ v1_gt1 v2_gt1 p1Dp2 cH.
rewrite !sum_beta_S //.
rewrite -addnA -addnCA addnC !addnA -addnA leq_add //.
  rewrite leq_eqVlt; apply/orP; left; apply/eqP.
  rewrite -addnn !dsum_alphaLE -!big_split /=; apply: eq_bigr ⇒ i _.
  rewrite !ffunE; set v := trshift _ _.
  have /subsetP := cH ⇒ /(_ (f v) (codom_f _ _)).
  rewrite !inE addnn.
  case: eqP ⇒ /= x1; case: eqP ⇒ /= x2; rewrite ?(mul1n, add0n, addn0) //.
  by move/eqP: x2; rewrite x1 (negPf p1Dp2).
  have /subsetP/(_ (f ord_max) (codom_f _ _)) := cH.
rewrite !inE.
case: eqP ⇒ /= x1; case: eqP ⇒ /= x2 // _; rewrite ?(mul1n, add0n, addn0) //;
     apply: (increasingE (increasing_alphaL_l _)).
  by apply: leq_maxr.
by apply: leq_maxl.
Qed.

Section Case1.

Definition sd n l (u : {ffun 'I_l.+1 → configuration 4 n}) :=
    \sum_(i < l) `d[u (inord i), u (inord i.+1)]_smove.

Variable n : nat.
Hypothesis IH:
     ∀ (l : nat) (p1 p2 p3 : ordinal_eqType 4)
       (u : {ffun 'I_l.+1 → configuration 4 n.+1}),
     p1 != p2 →
     p1 != p3 →
     p2 != p3 →
     p1 != p0 →
     p2 != p0 →
     p3 != p0 →
     (∀ k : 'I_l.+1,
      0 < k < l → codom (u k) \subset [:: p2; a[p1, p3] k]) →
     (S_[l] n.+1).*2 ≤ sd u +
                     sp (u ord0) l (a[p1, p3] 0) +
                     sp (u ord_max) l (a[p1, p3] l).

Variable l : nat.
Variables p1 p2 p3: peg 4.
Variable u : {ffun 'I_l.+2 → configuration 4 n.+2}.
Hypothesis p1Dp2 : p1 != p2.
Hypothesis p1Dp3 : p1 != p3.
Hypothesis p2Dp3 : p2 != p3.
Hypothesis p1Dp0 : p1 != p0.
Hypothesis p2Dp0 : p2 != p0.
Hypothesis p3Dp0 : p3 != p0.
Hypothesis cH : ∀ k : 'I_l.+2,
     0 < k < l.+1 → codom (u k) \subset [:: p2; a[p1, p3] k].

Let u':= ([ffun i ⇒ ↓[u i]] : {ffun 'I_l.+2 → configuration 4 n.+1})
 : {ffun 'I_l.+2 → configuration 4 n.+1}.

Let H: ∀ k : 'I_l.+2,
    0 < k < l.+1 → codom (u' k) \subset [:: p2; a[p1, p3] k].
Proof. by move⇒ k kH; rewrite ffunE; apply/codom_liftr/cH. Qed.

Let apeg13D2 a : a[p1, p3] a != p2.
Proof. by rewrite /apeg; case: odd; rewrite // eq_sym. Qed.

Let apeg13D0 a : a[p1, p3] a != p0.
Proof. by rewrite /apeg; case: odd; rewrite // eq_sym. Qed.

Hypothesis KH1 : u ord0 ord_max = p1.
Hypothesis KH2 : u ord_max ord_max != a[p3, p1] l.
Hypothesis l_gt0 : l != 0.

Lemma case1 :
  (S_[l.+1] n.+2).*2 ≤
  sd u + sp (u ord0) l.+1 p1 +
         sp (u ord_max) l.+1 (a[p3, p1] l).
Proof.
have il1E : inord l.+1 = ord_max :> 'I_l.+2
  by apply/val_eqP; rewrite /= inordK.
have iE : ∃ i, u (inord i) ord_max != a[p1, p3] i.
  by ∃ l.+1; rewrite apegS il1E.
case: (@ex_minnP _ iE) ⇒ a aH aMin.
have aMin1 i : i < a → u (inord i) ord_max = a[p1, p3] i.
  by case: (u (inord i) ord_max =P a[p1, p3] i) ⇒ // /eqP /aMin; case: leqP.
have aLld1 : a ≤ l.+1 by apply: aMin; rewrite apegS il1E.
have a_gt0 : 0 < a by case: (a) aH; rewrite // apeg0 -KH1 inord_eq0 //= eqxx.
pose ai : 'I_l.+2 := inord a.
have aiE : ai = a :> nat by rewrite inordK.
pose b := l.+1 - a.
pose bi : 'I_l.+2 := inord b.
have biE : bi = b :> nat by rewrite inordK // /b ltn_subLR // leq_addl.
have l_ggt0 : 0 < l by case: l l_gt0.
have [/andP[a_gt1 aLlm1]|] := boolP (2 ≤ a ≤ l.-1).
  have aLl : a ≤ l by rewrite (leq_trans aLlm1) // -subn1 leq_subr.
  have b_gt1 : 1 < b by rewrite leq_subRL // addn2 ltnS -[l]prednK.
  have uaiLEp2 : u ai ldisk = p2.
    have /cH/subsetP/(_ (u ai ldisk) (codom_f _ _)) : 0 < ai < l.+1.
      by rewrite aiE (leq_trans _ a_gt1) //= ltnS (leq_trans aLl1)
                 // ssrnat.leq_pred.
    by rewrite !inE aiE (negPf aH) orbF ⇒ /eqP.
  pose si i : configuration 4 n.+1 :=
     sgdist1 p2 (u (inord i)) (u (inord i.+1)).
  pose ti i : configuration 4 n.+1 :=
     sgdist2 p2 (u (inord i)) (u (inord i.+1)).
  have sitiH i : i < a.-1 →
     [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ],
         codom (ti i) \subset [:: u (inord i) ldisk; p2] &
         `d[u (inord i), u (inord i.+1)]_smove =
           D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2].
    move⇒ iLa.
    have iLa1 : i < a by rewrite (leq_trans iLa) // ssrnat.leq_pred.
    apply: sgdistE ⇒ //.
    - by rewrite aMin1.
    - rewrite !aMin1 //; last by rewrite -[a]prednK.
      by rewrite apegS apeg_eqC.
    - by rewrite aMin1 1?eq_sym // -[a]prednK.
    - by rewrite aMin1.
    by rewrite aMin1 // -[a]prednK.
  pose sam1 : configuration 4 n.+1 :=
     sgdist1 (a[p1, p3] a) (u (inord a.-1)) (u (inord a)).
  pose tam1 : configuration 4 n.+1 :=
     sgdist2 (a[p1, p3] a) (u (inord a.-1)) (u (inord a)).
  have [sam1C tam1C duam1ua1E] :
     [/\ codom sam1 \subset [:: a[p1, p3] a; u (inord a) ldisk ],
         codom tam1 \subset [:: u (inord a.-1) ldisk; a[p1, p3] a] &
         `d[u (inord a.-1), u (inord a)]_smove =
           D[[:: ↓[u (inord a.-1)]; sam1; tam1; ↓[u (inord a)]]].+2].
    apply: sgdistE ⇒ //.
    - by rewrite aMin1 ?prednK // -{2}[a]prednK //= apegS apeg_eqC.
    - by rewrite uaiLEp2 aMin1 ?prednK.
    - by rewrite uaiLEp2.
    - by rewrite aMin1 ?prednK.
    by rewrite uaiLEp2.
  have {}tam1C : codom tam1 \subset [:: p1; p3].
    move: tam1C; rewrite aMin1; last by rewrite -{2}[a]prednK.
    rewrite -subn1 apegO oddB //= [a[_, _]a]apegO; case: odd ⇒ //=.
    by rewrite codom_subC.
  pose u1 :=
    [ffun i ⇒
    if ((i : 'I_(3 × a).-2.+1) == 3 × a.-1 :>nat) then ↓[u (inord a.-1)]
    else if (i == (3 × a.-1).+1 :>nat) then sam1
    else if (i %% 3) == 0 then ↓[u (inord (i %/ 3))]
    else if (i %% 3) == 1 then si (i %/ 3)
    else ti (i %/ 3)].
  have u10E : u1 ord0 = ↓[u ord0].
    rewrite ffunE /= ifN ?inord_eq0 //.
    by rewrite neq_ltn muln_gt0 /= -ltnS prednK //= a_gt1.
  have uiME : u1 ord_max = sam1.
    rewrite ffunE /= eqn_leq leqNgt -{2}[a]prednK // mulnS.
    rewrite addSn add2n ltnS leqnn /=.
    by rewrite -{1}[a]prednK // mulnS eqxx.
  pose u2 := [ffun i : 'I_3 ⇒
    if i == 0 :> nat then sam1 else
    if i == 1 :> nat then tam1 else ↓[u ai]].
  pose u3 := [ffun i ⇒ ↓[u (inord ((i : 'I_b.+1) + a))]].
  have P1 : a.*2 + sd u1 + sd u2 + sd u3 ≤ sd u.
    have G b1 : b1 = a →
      \sum_(i < (3 × b1).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove =
      \sum_(i < (3 × a.-1)) `d[u1 (inord i), u1 (inord i.+1)]_smove +
      `d[↓[u (inord a.-1)], sam1]_smove.
      move⇒ b1Ea.
      have ta2E : (3 × b1).-2 = (3 × a.-1).+1.
        by rewrite b1Ea -{1}[a]prednK // mulnS.
      rewrite ta2E big_ord_recr /=; congr (_ + `d[_,_]_smove).
        by rewrite ffunE ifT// inordK // -{2}b1Ea ?ta2E.
      rewrite ffunE inordK; last by rewrite -{2}b1Ea ?ta2E.
      by rewrite eqn_leq ltnn /= eqxx.
    rewrite {}[sd u1]G //.
    have → := @sum3E _ (fun i ⇒ `d[u1 (inord i), u1 (inord i.+1)]_smove).
    have → : a.*2 = 2 + \sum_(i < a.-1) 2.
      rewrite sum_nat_const /= cardT size_enum_ord.
      by rewrite muln2 -(doubleD 1) add1n prednK.
    rewrite !addnA -[2 + _ + _]addnA -big_split /=.
    rewrite [2 + _]addnC -!addnA 2![X in _ + X ≤ _]addnA addnA.
    have → : sd u =
      \sum_(i < a.-1) (`d[u (inord i), u (inord i.+1)]_smove) +
      `d[u (inord a.-1), u ai]_smove +
      \sum_(i < b) `d[u (inord (a +i)), u (inord (a + i.+1))]_smove.
      have F := big_mkord xpredT
                    (fun i ⇒ `d[u (inord i), u (inord i.+1)]_smove).
      rewrite -{}[sd u]F.
      rewrite (big_cat_nat _ _ _ (_ : _ ≤ (a.-1).+1)) //=; last first.
         by rewrite prednK.
      rewrite big_mkord big_ord_recr /= prednK //.
      rewrite -{9}[a]add0n big_addn -/b big_mkord.
      congr (_ + _ + _).
      by apply: eq_bigr ⇒ i; rewrite addnC addnS.
    apply: leq_add; first apply: leq_add.
    - rewrite leq_eqVlt; apply/orP; left; apply/eqP.
      apply: eq_bigr ⇒ i _.
      have → : u1 (inord (3 × i)) = ↓[u (inord i)].
        rewrite ffunE inordK; last first.
          rewrite ltnS (leq_trans (_ : _ ≤ 3 × (a.-1))) //.
            by rewrite leq_mul2l /= ltnW.
          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.
        rewrite eqn_mul2l /= eqn_leq [_ ≤ i]leqNgt ltn_ord andbF.
        rewrite eqn_leq ltn_mul2l /= ltnNge [i ≤ _]ltnW // andbF.
        by rewrite mod3E eqxx mulKn.
      have → : u1 (inord (3 × i).+1) = si i.
        rewrite ffunE inordK; last first.
          rewrite ltnS (leq_trans (_ : _ ≤ 3 × (a.-1))) //.
            by rewrite ltn_mul2l /=.
          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.
        rewrite eqn_leq [_ ≤ _.+1]leqNgt.
        rewrite (leq_trans (_ : (3 × i).+2 ≤ (3 × i.+1))) ?andbF //;
               last 2 first.
        - by rewrite mulnS addSn add2n.
        - by rewrite leq_mul2l /=.
        rewrite eqn_leq !ltnS [_ ≤ 3 × i]leq_mul2l.
        by rewrite [_ ≤ i]leqNgt ltn_ord andbF mod3E /= div3E.
      have → : u1 (inord (3 × i).+2) = ti i.
        rewrite ffunE inordK; last first.
          rewrite ltnS (leq_trans (_ : _ ≤ 3 × (a.-1))) //.
            rewrite (leq_trans (_ : _ ≤ 3 × (i.+1))) //.
              by rewrite mulnS addSn add2n.
            by rewrite leq_mul2l /=.
          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.
        rewrite eqn_leq [_ ≤ _.+1]leqNgt.
        rewrite -[(3 × i).+3](mulnDr 3 1 i) leq_mul2l ltn_ord andbF.
        rewrite eqn_leq !ltnS [_ ≤ _.+1]leqNgt.
        rewrite (leq_trans (_ : (3 × i).+1 < 3 × (i.+1))) ?andbF //;
             last 2 first.
        - by rewrite mulnS addSn add2n.
        - by rewrite leq_mul2l /=.
        by rewrite mod3E /= div3E.
      have → : u1 (inord (3 × i).+3) = ↓[u (inord i.+1)].
        have → : (3 × i).+3 = 3 × (i.+1) by rewrite mulnS addSn add2n.
        rewrite ffunE inordK; last first.
          rewrite ltnS (leq_trans (_ : _ ≤ 3 × (a.-1))) //.
            by rewrite leq_mul2l /=.
          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.
        rewrite eqn_mul2l /=; case: eqP ⇒ [->//|_].
        rewrite eqn_leq [_ ≤ 3 × i.+1]leqNgt ltnS leq_mul2l /= ltn_ord andbF.
        by rewrite mod3E /= div3E.
      case: (sitiH i) ⇒ // _ _ →.
      by rewrite add2n /= addnA addn0.
    - rewrite leq_eqVlt; apply/orP; left; apply/eqP.
      rewrite /sd !big_ord_recr big_ord0 //= add0n !addnA.
      have → : u2 (inord 0) = sam1 by rewrite ffunE /= inordK.
      have → : u2 (inord 1) = tam1 by rewrite ffunE /= inordK.
      have → : u2 (inord 2) = ↓[u ai] by rewrite ffunE /= inordK.
      by move: duam1ua1E; rewrite /= addn0 add2n !addnA !addSn.
    apply: leq_sum ⇒ i _.
    rewrite ffunE inordK; last by rewrite ltnS ltnW.
    rewrite ffunE inordK; last by rewrite ltnS.
    rewrite addSn [i + _]addnC addnS.
    by apply/gdist_cunlift/shanoi_connect.
  set x1P1 := sd _ in P1; set x2P1 := sd _ in P1.
  set x3P1 := sd _ in P1; set xP1 := sd _ in P1.
  rewrite -/xP1.
  have cH2 (k : 'I_(3 × a).-2.+1) :
      0 < k < (3 × a).-2 → codom (u1 k) \subset [:: p2; a[p1, p3] k].
    move⇒ /andP[k_gt0 k_lt].
    have kL3a1 : k ≤ (3 × a.-1).
      by rewrite -ltnS (leq_trans k_lt) // -{1}[a]prednK // mulnS.
    have kLa1 : k %/ 3 ≤ a.-1.
      by rewrite -(mulKn a.-1 (isT : 0 < 3)) leq_div2r.
    rewrite ffunE; case: eqP ⇒ [kH|/eqP kH].
      rewrite kH apegMr //.
      have := @H (inord a.-1); rewrite inordK //.
        rewrite ffunE; apply.
        by rewrite -ltnS prednK // a_gt1.
      by rewrite prednK // (leq_trans aLld1).
    have k3La2 : k %/ 3 ≤ a.-2.
      rewrite -ltnS [a.-2.+1]prednK //; last first.
        by rewrite -subn1 ltn_subRL.
      rewrite ltn_divLR // [_ × 3]mulnC.
      by move: kL3a1 kH; case: ltngtP.
    rewrite eqn_leq [_ ≤ k]leqNgt (leq_trans k_lt) ?andbF //; last first.
      by rewrite -{1}[a]prednK // mulnS addSn add2n.
    have k3La : k %/ 3 ≤ a.
      by rewrite (leq_trans kLa1) // -subn1 leq_subr.
    case: eqP ⇒ k3mH.
      apply: codom_liftr.
      rewrite {2}(divn_eq k 3) k3mH addn0 [in a[_,_] _]mulnC apegMr //.
      have := @cH (inord (k %/3)); rewrite inordK; last first.
        by rewrite (leq_ltn_trans k3La).
      apply.
      rewrite (leq_ltn_trans k3La) ?ltnS //.
      move: k_gt0; rewrite andbT {1}(divn_eq k 3) k3mH addn0 muln_gt0.
      by case/andP.
    case: eqP ⇒ k3mH1.
      case: (sitiH ((k %/ 3))) ⇒ /=.
        by rewrite -[a.-1]prednK // -ltnS prednK.
      set pp := u _ _; (suff <- : pp = a[p1, p3] k by []); rewrite {}/pp.
      set i := inord _; have <- : a[p1, p3] i = a[p1, p3] k.
        rewrite (divn_eq k 3) k3mH1 addn1 apegS mulnC apegMr //.
        by rewrite /i !inordK ?apegS //= !ltnS (leq_trans k3La).
      have H2 : (k %/ 3).+1 < l.+2 by rewrite !ltnS (leq_trans k3La).
      rewrite -(@aMin1 i); last first.
        rewrite !inordK // -{2}[a]prednK // ltnS // -[a.-1]prednK // .
        by rewrite -subn1 subn_gt0.
      congr (u _ _).
      by apply/val_eqP; rewrite /= !inordK.
    rewrite codom_subC.
    case: (sitiH ((k %/ 3))) ⇒ /= [|_].
      by rewrite -[a.-1]prednK // -ltnS prednK.
    set pp := u _ _; (suff <- : pp = a[p1, p3] k by []); rewrite {}/pp.
    set i := inord _; have <- : a[p1, p3] i = a[p1, p3] k.
      have k3mH2 : k %% 3 = 2.
        have := ltn_mod k 3; move: k3mH k3mH1.
        by case: modn ⇒ // [] [|[]].
      rewrite (divn_eq k 3) k3mH2 addn2 !apegS mulnC apegMr //.
        by rewrite /i !inordK ?apegS //= !ltnS (leq_trans k3La).
      have H2 : (k %/ 3) < l.+2 by rewrite !ltnS (leq_trans k3La).
      rewrite -(@aMin1 i); last by rewrite !inordK // -{2}[a]prednK .
      congr (u _ _).
      by apply/val_eqP; rewrite /= !inordK.
  have {cH2}P2 := IH p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0 cH2.
  have a3B2_gt1 : 1 < (3 × a).-2.
    rewrite -subn2 leq_subRL.
      by rewrite (leq_trans (_ : 4 ≤ 3 × 2)) // leq_mul2l.
    by rewrite (leq_trans (_ : 2 ≤ 3 × 2)) // leq_mul2l.
  rewrite u10E uiME apeg0 in P2.
  have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                          (leqnn _)).
  pose pa := a[p1, p3] a; pose paS := a[p1, p3] a.+1.
  have cH3 (k : 'I_3) :
    0 < k < 2 → codom (u2 k) \subset [:: paS; a[p2, pa] k].
    case: k ⇒ [] [|[|]] //= iH _.
    by rewrite /pa /paS !apegS apeg0 ffunE /= codom_apeg codom_subC.
  rewrite -/x1P1 in P2.
  have {cH3}P3 :
    (S_[2] n.+1).*2 ≤ sd u2 + sp (u2 ord0) 2 (a[p2, pa] 0) +
                       sp (u2 ord_max) 2 (a[p2, pa] 2).
    apply: IH cH3 ⇒ //; try by rewrite /pa /paS // eq_sym.
    by rewrite /pa /paS apegS apeg_eqC eq_sym.
  rewrite !ffunE /= apeg0 -/x2P1 in P3.
  have cH4 (k : 'I_b.+1) :
      0 < k < b → codom (u3 k) \subset [:: p2; a[pa, paS] k].
      rewrite /b .
    move⇒ /andP[k_gt0 kLb].
    have kBound : 0 < k + a < l.+1.
      rewrite (leq_trans a_gt0) ?leq_addl //=.
      by move: kLb; rewrite /b ltn_subRL addnC.
    rewrite ffunE codom_liftr //.
    have := @cH (inord (k + a)).
    rewrite /pa /paS apegS inordK; first by rewrite -apegD; apply.
    by rewrite ltnW // ltnS; case/andP: kBound.
  have {cH4}P4 :
   (S_[b] n.+1).*2 ≤ sd u3 + sp (u3 ord0) b (a[pa, paS] 0) +
                      sp (u3 ord_max) b (a[pa, paS] b).
    apply: IH cH4 ⇒ //; try by rewrite /pa /paS // eq_sym.
    by rewrite /pa /paS apegS apeg_eqC.
  have {}P4 := leq_trans P4 (leq_add (leqnn _) (leq_sum_beta _ _)).
  rewrite apeg0 /= (_ : a[_, _] b = a[p3, p1] l) in P4; last first.
    by rewrite /pa /paS apegS -apegD subnK ?apegS.
  rewrite !ffunE /= add0n -/ai in P4.
  rewrite -/x3P1 subnK // (_ : inord l.+1 = ord_max) in P4; last first.
    by apply/val_eqP; rewrite /= inordK.
  rewrite [X in _ ≤ _ + X + _]sum_beta_S //= KH1 eqxx addn0.
  set xS := \sum_(_ < _) _ in P2; rewrite -/xS.
  rewrite [X in _ ≤ _ + _ + X]sum_beta_S //= KH2 mul1n.
  set yS := \sum_(_ < _) _ in P4; rewrite -/yS.
  set x1S := sp _ _ _ in P2; set y1S := sp _ _ _ in P3.
  have x1Sy1SE : x1S + y1S ≤ (S_[1] n).*2 + α_[maxn (3 × a).-2 2] n.
    apply: sum_alpha_diffE ⇒ //.
    rewrite apeg32E //.
    by move: sam1C; rewrite -uiME uaiLEp2.
  rewrite (maxn_idPl _) // in x1Sy1SE.
  set x2S := sp _ _ _ in P3; set y2S := sp _ _ _ in P4.
  have x2y2SE : x2S + y2S ≤ (S_[1] n).*2 + α_[maxn 2 b] n.
    apply: sum_alpha_diffE ⇒ //; first by rewrite /pa eq_sym.
    have /H : 0 < (inord a : 'I_l.+2) < l.+1 by rewrite inordK // a_gt0.
    by rewrite ffunE inordK.
  rewrite -addnn {1}dsum_alphaL_S in P2.
  rewrite -addnn {1}dsum_alphaL_S in P3.
  rewrite -addnn {1}dsum_alphaL_S.
  have F4 k : S_[a.-1] k.+1 ≤ S_[(3 ×a).-2] k + a.-1.
    apply: leq_trans (dsum_alpha3l _ _) _.
    rewrite leq_add2r.
    apply: (increasingE (increasing_dsum_alphaL_l _)).
    by rewrite -{2}[a]prednK // mulnS addSn add2n /=.
  have F4n := F4 n.
  have {F4}F4n1 := F4 n.+1.
  have F5 k :
    S_[l.+1] k.+1 + S_[1] k.+1 + S_[b.+1] k.+1 ≤
    S_[a.-1] k.+1 + S_[b.+2] k.+1 + S_[b] k + (α_[1] k).*2.
    have <- : a + b = l.+1 by rewrite addnC subnK.
    rewrite -[X in _ ≤ X]addnA (leq_add _ (dsum_alphaL_alpha k b_gt1)) //.
    have := concaveEk1 1 a.-2 b.+1 (concave_dsum_alphaL_l k.+1).
    rewrite add1n prednK; last by rewrite -subn1 ltn_subRL addn0.
    by rewrite -addSnnS prednK // add1n [X in _ ≤ X]addnC.
  have F5n := F5 n.
  have {F5}F5n1 := F5 n.+1.
  have F6 k : S_[b.+2] k + S_[1] k ≤ S_[b.+1] k + S_[2] k.
    by have := concaveEk1 1 1 b (concave_dsum_alphaL_l k).
  have F6n := F6 n.+1.
  have {F6}F6n1 := F6 n.+2.
  have F72 := dsum_alphaL_S 2 n.+1.
  have F721 := dsum_alphaL_S 2 n.
  have F711 := dsum_alphaL_S 1 n.+1.
  have F71 := dsum_alphaL_S 1 n.
  have F73 := dsum_alphaL_S b n.
  have F8 : α_[2] n.+1 ≤ α_[1] n.+2.
    have ->: α_[1] n.+2 = α_[3] n.+1 by rewrite alphaL_3E.
    by apply: increasing_alphaL_l.
  have F9 : α_[1] (n.+2) ≤ (α_[1] n).*2.+2.
    apply: leq_trans (leqnSn _).
    by apply: alphaL_4_5.
  gsimpl.
  applyr P1.
  rewrite -(leq_add2r x1S); applyr P2.
  rewrite -(leq_add2r (y1S + x2S)); applyr P3.
  rewrite -(leq_add2r y2S); applyr P4.
  applyl x2y2SE; applyl x1Sy1SE.
  rewrite -[in 2 × a](prednK a_gt0).
  applyr F4n; applyr F4n1; gsimpl.
  rewrite (maxn_idPr _) //.
  rewrite -(leq_add2r (S_[1] n.+1 + S_[b.+1] n.+1)); applyl F5n.
  rewrite -(leq_add2r (S_[1] n.+2 + S_[b.+1] n.+2)); applyl F5n1.
  gsimpl.
  rewrite -(leq_add2r (S_[1] n.+1)); applyl F6n; gsimpl.
  rewrite F71; gsimpl.
  rewrite !add1n {}F73; gsimpl.
  rewrite -(leq_add2r (S_[1] n.+2 + S_[2] n.+2)).
  applyl F6n1; gsimpl.
  rewrite {}F72 {}F721 {}F711 {}F71; gsimpl.
  applyl F8.
  by applyl F9; gsimpl.
rewrite negb_and -leqNgt -ltnNge ⇒ oH.
have [/andP[a_gt1 /eqP bE1]|] := boolP ((1 < a) && (b == 1)).
  have am1_gt0 : 0 < a.-1 by rewrite -subn1 subn_gt0.
  have lEa : l = a.
    have : a + b = l.+1 by rewrite addnC subnK //.
    by rewrite bE1 addn1 ⇒ [] [].
  have uaiLEp2 : u ai ldisk = p2.
    have /cH/subsetP/(_ (u ai ldisk) (codom_f _ _)) : 0 < ai < l.+1.
      by rewrite aiE a_gt0 lEa /=.
    by rewrite !inE aiE (negPf aH) orbF ⇒ /eqP.
  pose si i : configuration 4 n.+1 :=
     sgdist1 p2 (u (inord i)) (u (inord i.+1)).
  pose ti i : configuration 4 n.+1 :=
     sgdist2 p2 (u (inord i)) (u (inord i.+1)).
  have sitiH i : i < a.-1 →
     [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ],
         codom (ti i) \subset [:: u (inord i) ldisk; p2] &
         `d[u (inord i), u (inord i.+1)]_smove =
           D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2].
    move⇒ iLa.
    have iLa1 : i < a by rewrite (leq_trans iLa) // ssrnat.leq_pred.
    apply: sgdistE ⇒ //.
    - by rewrite aMin1.
    - rewrite !aMin1 //; last by rewrite -[a]prednK.
      by rewrite apegS apeg_eqC.
    - by rewrite aMin1 1?eq_sym // -[a]prednK.
    - by rewrite aMin1.
    by rewrite aMin1 // -[a]prednK.
  pose pa := a[p1, p3] a.
  pose sam1 : configuration 4 n.+1 := sgdist1 pa (u (inord a.-1)) (u (inord a)).
  pose tam1 : configuration 4 n.+1 := sgdist2 pa (u (inord a.-1)) (u (inord a)).
  have [sam1C tam1C duam1ua1E] :
     [/\ codom sam1 \subset [:: pa; u (inord a) ldisk ],
         codom tam1 \subset [:: u (inord a.-1) ldisk; pa] &
         `d[u (inord a.-1), u (inord a)]_smove =
           D[[:: ↓[u (inord a.-1)]; sam1; tam1; ↓[u (inord a)]]].+2].
    apply: sgdistE; rewrite /pa //.
    - by rewrite aMin1 ?prednK // -{2}[a]prednK //= apegS apeg_eqC.
    - by rewrite uaiLEp2 aMin1 // prednK.
    - by rewrite uaiLEp2.
    - by rewrite aMin1 // prednK.
    by rewrite uaiLEp2.
  have {}tam1C : codom tam1 \subset [:: p1; p3].
    move: tam1C; rewrite aMin1; last by rewrite -{2}[a]prednK.
    by rewrite /pa -{2}[a]prednK // apegS codom_apeg.
  pose u1 :=
    [ffun i ⇒
    if ((i : 'I_(3 × a).-2.+1) == 3 × a.-1 :>nat) then ↓[u (inord a.-1)]
    else if (i == (3 × a.-1).+1 :>nat) then sam1
    else if (i %% 3) == 0 then ↓[u (inord (i %/ 3))]
    else if (i %% 3) == 1 then si (i %/ 3)
    else ti (i %/ 3)].
  have u10E : u1 ord0 = ↓[u ord0].
    rewrite ffunE /= ifN ?inord_eq0 //.
    by rewrite neq_ltn muln_gt0 /= -ltnS prednK //= a_gt1.
  have uiME : u1 ord_max = sam1.
    rewrite ffunE /= eqn_leq leqNgt -{2}[a]prednK // mulnS.
    rewrite addSn add2n ltnS leqnn /=.
    by rewrite -{1}[a]prednK // mulnS eqxx.
  pose u2 :=
    [ffun i : 'I_4 ⇒
    if i == 0 :> nat then sam1 else
    if i == 1 :> nat then tam1 else
    if i == 2 :> nat then ↓[u ai] else ↓[u (inord (l.+1))]].
  have P1 : a.*2 + sd u1 + sd u2 ≤ sd u.
    have G b1 : b1 = a →
      \sum_(i < (3 × b1).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove =
      \sum_(i < (3 × a.-1)) `d[u1 (inord i), u1 (inord i.+1)]_smove +
      `d[↓[u (inord a.-1)], sam1]_smove.
      move⇒ b1Ea.
      have ta2E : (3 × b1).-2 = (3 × a.-1).+1.
        by rewrite b1Ea -{1}[a]prednK // mulnS.
      rewrite ta2E big_ord_recr /=; congr (_ + `d[_,_]_smove).
        by rewrite ffunE ifT// inordK // -{2}b1Ea ?ta2E.
      rewrite ffunE inordK; last by rewrite -{2}b1Ea ?ta2E.
      by rewrite eqn_leq ltnn /= eqxx.
    rewrite {}[sd u1]G //.
    have → := @sum3E _ (fun i ⇒ `d[u1 (inord i), u1 (inord i.+1)]_smove).
    have → : a.*2 = 2 + \sum_(i < a.-1) 2.
      rewrite sum_nat_const /= cardT size_enum_ord.
      by rewrite muln2 -(doubleD 1) add1n prednK.
    rewrite !addnA -[2 + _ + _]addnA -big_split /=.
    rewrite [sd u2]big_ord_recr /=.
    rewrite [u2 (inord 2)]ffunE inordK //=.
    rewrite [u2 (inord 3)]ffunE inordK //=.
    rewrite [2 + _]addnC -!addnA 2![X in _ + X ≤ _]addnA addnA.
    have → : sd u =
      \sum_(i < a.-1) (`d[u (inord i), u (inord i.+1)]_smove) +
      `d[u (inord a.-1), u ai]_smove + `d[u ai, u (inord ai.+1)]_smove.
      rewrite -lEa (_ : ai = inord l); last first.
        by apply/val_eqP; rewrite /= aiE inordK // lEa.
      case: l l_gt0 u ⇒ //= l1 _ f.
      rewrite /sd 2!big_ord_recr //=; congr (_ + _ + `d[f _, f _]_smove).
      by apply/val_eqP; rewrite /= !inordK.
    apply: leq_add; first apply: leq_add.
    - rewrite leq_eqVlt; apply/orP; left; apply/eqP.
      apply: eq_bigr ⇒ i _.
      have → : u1 (inord (3 × i)) = ↓[u (inord i)].
        rewrite ffunE inordK; last first.
          rewrite ltnS (leq_trans (_ : _ ≤ 3 × (a.-1))) //.
            by rewrite leq_mul2l /= ltnW.
          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.
        rewrite eqn_mul2l /= eqn_leq [_ ≤ i]leqNgt ltn_ord andbF.
        rewrite eqn_leq ltn_mul2l /= ltnNge [i ≤ _]ltnW // andbF.
        by rewrite mod3E /= div3E.
      have → : u1 (inord (3 × i).+1) = si i.
        rewrite ffunE inordK; last first.
          rewrite ltnS (leq_trans (_ : _ ≤ 3 × (a.-1))) //.
            by rewrite ltn_mul2l /=.
          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.
        rewrite eqn_leq [_ ≤ _.+1]leqNgt.
        rewrite (leq_trans (_ : (3 × i).+2 ≤ (3 × i.+1))) ?andbF //;
               last 2 first.
        - by rewrite mulnS addSn add2n.
        - by rewrite leq_mul2l /=.
        rewrite eqn_leq !ltnS [_ ≤ 3 × i]leq_mul2l.
        by rewrite [_ ≤ i]leqNgt ltn_ord andbF mod3E /= div3E.
      have → : u1 (inord (3 × i).+2) = ti i.
        rewrite ffunE inordK; last first.
          rewrite ltnS (leq_trans (_ : _ ≤ 3 × (a.-1))) //.
            rewrite (leq_trans (_ : _ ≤ 3 × (i.+1))) //.
              by rewrite mulnS addSn add2n.
            by rewrite leq_mul2l /=.
          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.
        rewrite eqn_leq [_ ≤ _.+1]leqNgt.
        rewrite -[(3 × i).+3](mulnDr 3 1 i) leq_mul2l ltn_ord andbF.
        rewrite eqn_leq !ltnS [_ ≤ _.+1]leqNgt.
        rewrite (leq_trans (_ : (3 × i).+1 < 3 × (i.+1))) ?andbF //;
             last 2 first.
        - by rewrite mulnS addSn add2n.
        - by rewrite leq_mul2l /=.
        by rewrite mod3E /= div3E.
      have → : u1 (inord (3 × i).+3) = ↓[u (inord i.+1)].
        have → : (3 × i).+3 = 3 × (i.+1) by rewrite mulnS addSn add2n.
        rewrite ffunE inordK; last first.
          rewrite ltnS (leq_trans (_ : _ ≤ 3 × (a.-1))) //.
            by rewrite leq_mul2l /=.
          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.
        rewrite eqn_mul2l /=; case: eqP ⇒ [->//|_].
        rewrite eqn_leq [_ ≤ 3 × i.+1]leqNgt ltnS leq_mul2l /= ltn_ord andbF.
        by rewrite mod3E /= div3E.
      case: (sitiH i) ⇒ //= _ _.
      by rewrite !addnA addn0 add2n.
    - rewrite leq_eqVlt; apply/orP; left; apply/eqP.
      rewrite !big_ord_recr big_ord0 //= add0n !addnA.
      have → : u2 (inord 0) = sam1 by rewrite ffunE /= inordK.
      have → : u2 (inord 1) = tam1 by rewrite ffunE /= inordK.
      have → : u2 (inord 2) = ↓[u ai] by rewrite ffunE /= inordK.
      by move: duam1ua1E; rewrite /= addn0 add2n !addnA !addSn.
    rewrite (_ : inord l.+1 = inord ai.+1); last first.
      by apply/val_eqP; rewrite /= !inordK // lEa.
    by apply/gdist_cunlift/shanoi_connect.
  set x1P1 := sd _ in P1; set x2P1 := sd _ in P1.
  set xP1 := sd _ in P1; rewrite -/xP1.
  have cH2 (k : 'I_(3 × a).-2.+1) :
      0 < k < (3 × a).-2 → codom (u1 k) \subset [:: p2; a[p1, p3] k].
    move⇒ /andP[k_gt0 k_lt].
    have kL3a1 : k ≤ (3 × a.-1).
      by rewrite -ltnS (leq_trans k_lt) // -{1}[a]prednK // mulnS.
    have kLa1 : k %/ 3 ≤ a.-1.
      by rewrite -(mulKn a.-1 (isT : 0 < 3)) leq_div2r.
    rewrite ffunE; case: eqP ⇒ [kH|/eqP kH].
      rewrite kH apegMr //.
      have := @H (inord a.-1); rewrite inordK //.
        rewrite ffunE; apply.
        by rewrite -ltnS prednK // a_gt1.
      by rewrite prednK // (leq_trans aLld1).
    have k3La2 : k %/ 3 ≤ a.-2.
      rewrite -ltnS [a.-2.+1]prednK //.
      rewrite ltn_divLR // [_ × 3]mulnC.
      by move: kL3a1 kH; case: ltngtP.
    rewrite eqn_leq [_ ≤ k]leqNgt (leq_trans k_lt) ?andbF //; last first.
      by rewrite -{1}[a]prednK // mulnS addSn add2n.
    have k3La : k %/ 3 ≤ a.
      by rewrite (leq_trans kLa1) // -subn1 leq_subr.
    case: eqP ⇒ k3mH.
      apply: codom_liftr.
      rewrite {2}(divn_eq k 3) k3mH addn0 [in a[_,_] _]mulnC apegMr //.
      have := @cH (inord (k %/3)); rewrite inordK; last first.
        by rewrite (leq_ltn_trans k3La).
      apply.
      rewrite (leq_ltn_trans k3La) ?ltnS ?lEa //.
      move: k_gt0; rewrite andbT {1}(divn_eq k 3) k3mH addn0 muln_gt0.
      by case/andP.
    case: eqP ⇒ k3mH1.
      case: (sitiH (k %/ 3)); first by rewrite -[a.-1]prednK.
      set pp := u _ _; (suff <- : pp = a[p1, p3] k by []); rewrite {}/pp.
      set i := inord _; have <- : a[p1, p3] i = a[p1, p3] k.
        rewrite (divn_eq k 3) k3mH1 addn1 apegS mulnC apegMr //.
        by rewrite /i !inordK ?apegS //= !ltnS lEa.
      have H2 : (k %/ 3).+1 < l.+2 by rewrite !ltnS lEa (leq_trans k3La).
      rewrite -(@aMin1 i); last first.
        by rewrite !inordK // -{2}[a]prednK // ltnS // -[a.-1]prednK.
      congr (u _ _).
      by apply/val_eqP; rewrite /= !inordK.
    rewrite codom_subC.
    case: (sitiH (k %/ 3)) ⇒ [|_]; first by rewrite -[a.-1]prednK.
    set pp := u _ _; (suff <- : pp = a[p1, p3] k by []); rewrite {}/pp.
    set i := inord _; have <- : a[p1, p3] i = a[p1, p3] k.
      have k3mH2 : k %% 3 = 2.
        have := ltn_mod k 3; move: k3mH k3mH1.
        by case: modn ⇒ // [] [|[]].
      rewrite (divn_eq k 3) k3mH2 addn2 !apegS mulnC apegMr //.
        by rewrite /i !inordK ?apegS //= !ltnS (leq_trans k3La).
      have H2 : (k %/ 3) < l.+2 by rewrite !ltnS (leq_trans k3La).
      rewrite -(@aMin1 i); last by rewrite !inordK // -{2}[a]prednK .
      congr (u _ _).
      by apply/val_eqP; rewrite /= !inordK.
  have {cH2}P2 := IH p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0 cH2.
  have a3B2_gt1 : 1 < (3 × a).-2.
    rewrite -subn2 leq_subRL.
      by rewrite (leq_trans (_ : 4 ≤ 3 × 2)) // leq_mul2l.
    by rewrite (leq_trans (_ : 2 ≤ 3 × 2)) // leq_mul2l.
  rewrite u10E uiME apeg0 in P2.
  have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                          (leqnn _)).
  rewrite -/x1P1 in P2.
  pose paS := a[p1, p3] a.+1.
  have cH3 (k : 'I_4) :
    0 < k < 3 → codom (u2 k) \subset [:: pa; a[p2, paS] k].
    case: k ⇒ [] [|[|[|]]] //= iH _; rewrite ffunE /=.
      by have := tam1C; rewrite /pa /paS !(apegS, apeg0) codom_apeg.
    apply: codom_liftr.
    have /cH : 0 < ai < l.+1 by rewrite aiE a_gt0 // lEa /=.
    by rewrite /pa /paS !(apegS, apeg0) aiE codom_subC.
  have {cH3}P3 :
    (S_[3] n.+1).*2 ≤ sd u2 + sp (u2 ord0) 3 (a[p2, paS] 0) +
                       sp (u2 ord_max) 3 (a[p2, paS] 3).
    apply: IH cH3 ⇒ //; try by rewrite /pa /paS // eq_sym.
    by rewrite /paS apegS apeg_eqC.
  have {}P3 := leq_trans P3 (leq_add (leqnn _) (leq_sum_beta _ _)).
  rewrite /pa /paS -lEa !(apegS, apeg0) in P3.
  rewrite !ffunE /= -/x2P1 (_ : inord l.+1 = ord_max) in P3; last first.
    by apply/val_eqP; rewrite /= inordK.
  rewrite [X in _ ≤ _ + X + _]sum_beta_S //= KH1 eqxx addn0.
  set xS := \sum_(_ < _) _ in P2; rewrite -/xS.
  rewrite [X in _ ≤ _ + _ + X]sum_beta_S //= KH2 mul1n.
  set yS := \sum_(i < _) _ in P3; rewrite -/yS.
  set x1S := sp _ _ _ in P2; set y1S := sp _ _ _ in P3.
  have x1Sy1SE : x1S + y1S ≤ (S_[1] n).*2 + α_[maxn (3 × a).-2 3] n.
    apply: sum_alpha_diffE ⇒ //.
    by move: sam1C; rewrite -uiME uaiLEp2 /pa apeg32E.
  rewrite (maxn_idPl _) // in x1Sy1SE; last first.
    by rewrite -subn2 ltn_subRL ltnW // (leq_mul2l 3 2).
  rewrite -addnn {1}dsum_alphaL_S in P2.
  rewrite -addnn {1}dsum_alphaL_S.
  have F4 k : S_[a.-1] k.+1 ≤ S_[(3 ×a).-2] k + a.-1.
    apply: leq_trans (dsum_alpha3l _ _) _.
    rewrite leq_add2r.
    apply: (increasingE (increasing_dsum_alphaL_l _)).
    by rewrite -{2}[a]prednK // mulnS addSn add2n /=.
  have F4n := F4 n.
  have {F4}F4n1 := F4 n.+1.
  have F6 k : S_[a.+1] k + S_[1] k ≤ S_[a.-1] k + S_[3] k.
    have := concaveEk1 1 a.-2 2 (concave_dsum_alphaL_l k).
    by rewrite add1n addn2 !prednK // [_ + S_[3] _]addnC.
  have F6n := F6 n.+1.
  have {F6}F6n1 := F6 n.+2.
  have F72 := dsum_alphaL_S 3 n.+1.
  have F721 := dsum_alphaL_S 3 n.
  have F711 := dsum_alphaL_S 1 n.+1.
  have F71 := dsum_alphaL_S 1 n.
  have F8 : α_[1] n.+2 = α_[3] n.+1 by rewrite alphaL_3E.
  have F9 : α_[1] (n.+2) ≤ (α_[1] n).*2.+2.
    apply: leq_trans (leqnSn _).
    by apply: alphaL_4_5.
  gsimpl.
  applyr P1.
  rewrite -(leq_add2r x1S); applyr P2.
  rewrite -(leq_add2r y1S); applyr P3.
  applyl x1Sy1SE; gsimpl.
  rewrite -(leq_add2r (S_[a.-1] n.+1)) -[in 2 × a](prednK a_gt0).
  applyl F4n.
  rewrite -(leq_add2r (S_[a.-1] n.+2)); applyl F4n1.
  rewrite lEa; applyr F6n.
  rewrite -(leq_add2r (S_[1] n.+2 + S_[3] n.+2)); applyr F6n1.
  rewrite {}F72 {}F711 {}F71; gsimpl.
  rewrite !add1n -{}F8.
  by applyl F9; gsimpl.
rewrite negb_and -leqNgt ⇒ o1H.
have [/eqP aE1| aD1] := boolP (a == 1).
  have b_gt0 : 0 < b by rewrite /b aE1 subn1.
  have bE : b = l by rewrite /b aE1 subn1.
  move: b_gt0; rewrite leq_eqVlt ⇒ /orP[/eqP bE1 | b_gt1]; last first.
    have u1C : u (inord 1) ldisk = p2.
      move: aH; rewrite aE1 apegS apeg0.
      have /cH : 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK.
      move⇒ /subsetP/(_ (u (inord 1) ldisk) (codom_f _ _)).
      by rewrite !inE ⇒ /orP[] /eqP→ //; rewrite !inordK // apegS apeg0 eqxx.
    pose s0 : configuration 4 n.+1 := sgdist1 p3 (u ord0) (u (inord 1)).
    pose t0 : configuration 4 n.+1 := sgdist2 p3 (u ord0) (u (inord 1)).
    have [s0C t0C ds0t0E] :
        [/\ codom s0 \subset [:: p3; u (inord 1) ldisk ],
         codom t0 \subset [:: u ord0 ldisk; p3] &
         `d[u ord0, u (inord 1)]_smove =
           D[[:: ↓[u ord0]; s0; t0; ↓[u (inord 1)]]].+2].
      apply: sgdistE ⇒ //.
      - by rewrite /= KH1.
      - by rewrite KH1 u1C.
      - by rewrite u1C eq_sym.
      - by rewrite KH1.
      by rewrite u1C.
    pose u1 :=
      [ffun i : 'I_4 ⇒
      if i == 0 :> nat then ↓[u ord0] else
      if i == 1 :> nat then s0 else
      if i == 2 :> nat then t0 else ↓[u (inord 1)]].
    pose u2 := [ffun i ⇒ ↓[u (inord ((i : 'I_b.+1) + 1))]].
    have P1 : 2 + sd u1 + sd u2 ≤ sd u.
      have → : sd u =
          `d[u ord0, u (inord 1)]_smove +
          \sum_(i < b) `d[u (inord (a +i)), u (inord (a + i.+1))]_smove.
        rewrite /sd big_ord_recl /= bE.
        congr (`d[u _,u _]_smove + _).
          by apply/val_eqP; rewrite /= inordK.
        apply: eq_bigr ⇒ i _.
        congr (`d[u _,u _]_smove); apply/val_eqP; rewrite aE1 /= inordK //=.
          by rewrite /bump add1n !ltnS ltnW.
        by rewrite /bump add1n !ltnS.
      apply: leq_add.
        rewrite leq_eqVlt; apply/orP; left; apply/eqP.
        rewrite /sd !big_ord_recr /= big_ord0 add0n.
        rewrite !ffunE !inordK //= add2n.
        by rewrite ds0t0E /= addn0 !addnA.
      apply: leq_sum ⇒ i _.
      rewrite ffunE inordK; last by rewrite ltnS ltnW.
      rewrite ffunE inordK; last by rewrite ltnS.
      rewrite aE1 addSn [i + _]addnC addnS.
      by apply/gdist_cunlift/shanoi_connect.
    set x1P1 := sd _ in P1; set x2P1 := sd _ in P1.
    set xP1 := sd _ in P1; rewrite -/xP1.
    have cH2 (k : 'I_4) :
      0 < k < 3 → codom (u1 k) \subset [:: p3; a[p1, p2] k].
      case: k ⇒ [] [|[|[|]]] //= iH _; rewrite ffunE /= !(apegS, apeg0).
        by have := s0C; rewrite u1C.
      by rewrite codom_subC -KH1.
    have {cH2}P2 :
      (S_[3] n.+1).*2 ≤ sd u1 + sp ↓[u (inord 0)] 3 (a[p1, p2] 0) +
                         sp ↓[u (inord 1)] 3 (a[p1, p2] 3).
      apply: leq_trans (IH _ _ _ _ _ _ cH2) _ ⇒ //.
        by rewrite eq_sym.
      repeat apply: leq_add ⇒ //; rewrite leq_eqVlt;
             apply/orP; left; apply/eqP.
        by apply: eq_bigr ⇒ i _; rewrite !ffunE inord_eq0.
      by apply: eq_bigr ⇒ i _; rewrite !ffunE.
    have {}P2 := leq_trans P2
               (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leqnn _)).
    rewrite -/x2P1 (inord_eq0) // -[in inord 1]aE1 !(apegS, apeg0) in P2.
    have cH3 (k : 'I_b.+1) :
      0 < k < b → codom (u2 k) \subset [:: p2; a[p3, p1] k].
      rewrite [X in k < X]bE ⇒ /andP[k_gt0 kLb].
      rewrite ffunE addn1; apply: codom_liftr.
      have := @cH (inord k.+1).
      rewrite inordK ?apegS //=; first by apply.
      by rewrite ltnS (leq_trans kLb).
    have {cH3}P3 :
     (S_[b] n.+1).*2 ≤ sd u2 + sp ↓[u (inord 1)] b p3 +
                        sp ↓[u ord_max] b (a[p3, p1] b).
      apply: leq_trans (IH _ _ _ _ _ _ cH3) _ ⇒ //; try by rewrite eq_sym.
      repeat apply: leq_add ⇒ //; rewrite leq_eqVlt;
         apply/orP; left; apply/eqP; apply: eq_bigr ⇒ i _.
        by rewrite !ffunE.
      rewrite !ffunE /= addn1 bE; congr ((u _ _ != _) × _).
      by apply/val_eqP; rewrite /= inordK.
    have {}P3 := leq_trans P3 (leq_add (leqnn _) (leq_sum_beta _ _)).
    rewrite -/x2P1 (_ : a[p3, p1] b = a[p3, p1] l) in P3; last first.
      by rewrite bE.
    rewrite -[in inord 1]aE1 in P3.
    rewrite !sum_beta_S // KH1 eqxx mul0n addn0 KH2 mul1n.
    set xS := \sum_(i < _) _ in P2; rewrite -/xS.
    set yS := \sum_(i < _) _ in P3; rewrite -/yS.
    set x1S := sp _ _ _ in P2; set y1S := sp _ _ _ in P3.
    have x1Sy1SE : x1S + y1S ≤ (S_[1] n).*2 + α_[maxn 3 b] n.
      apply: sum_alpha_diffE ⇒ //.
      apply: codom_liftr.
      have /cH : 0 < (inord a : 'I_l.+2) < l.+1 by rewrite aE1 inordK.
      by rewrite inordK aE1.
    rewrite -/x1P1 in P2.
    rewrite -addnn {1}dsum_alphaL_S -bE.
    gsimpl; applyr P1.
    rewrite -(leq_add2r x1S); applyr P2.
    rewrite -(leq_add2r y1S); applyr P3.
    applyl x1Sy1SE; gsimpl.
    move: b_gt1; rewrite leq_eqVlt ⇒ /orP[/eqP bE2|b_gt2].
      rewrite -bE2 (maxn_idPl _) //.
      rewrite [S_[3] n.+2]dsum_alphaL_S; gsimpl.
      rewrite !alphaL_3E.
      have F := leq_dsum_alpha_2l_1 n.+1; applyr F.
      rewrite !dsum_alphaL_S; gsimpl.
      rewrite !add1n.
      by have F := alphaL_4_5 n; applyl F; gsimpl.
    rewrite (maxn_idPr _) //.
    changer (2 × (S_[3] (n.+1)).+1 + 2 × S_[b] (n.+1)).
    rewrite -dsum_alpha3_S.
    rewrite ![in X in _ ≤ 2 × X + _]dsum_alphaL_S; gsimpl.
    rewrite [in X in _ ≤ _ + X]mul2n -addnn.
    rewrite [in X in _ ≤ _ + (X + _)]dsum_alphaL_S; gsimpl.
    changer ((S_[b] n + (α_[1] n).*2) + (S_[b] n.+1 + (α_[1] n.+1).*2)).
    by apply: leq_add; apply: dsum_alphaL_alpha; apply: ltnW.
  have /cH : 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK.
  move⇒ /subsetP /(_ (u (inord 1) ldisk) (codom_f _ _)).
  rewrite !inE inordK // apegS apeg0.
  have := aH; rewrite (_ : inord a = inord 1); last first.
    by apply/val_eqP; rewrite /= !inordK // aE1.
  rewrite aE1 apegS ⇒ /negPf->; rewrite orbF ⇒ /eqP u1LE.
  case: (@sgdistE _ p3 (u ord0) (u (inord 1))) ⇒ //.
  - by rewrite KH1.
  - by rewrite KH1 u1LE.
  - by rewrite u1LE eq_sym.
  - by rewrite KH1.
  by rewrite u1LE.
  set s0 := sgdist1 _ _ _; set t0 := sgdist2 _ _ _.
  move⇒ s0C t0C du0u1; rewrite /= !addnA addn0 in du0u1.
  pose u1 :=
    [ffun i ⇒
      if (i : 'I_5) == 0 :> nat then ↓[u ord0] else
      if i == 1 :> nat then s0 else
      if i == 2 :> nat then t0 else
      if i == 3 :> nat then ↓[u (inord 1)] else ↓[u (inord 2)]].
  have P1 : 2 + sd u1 ≤ sd u.
    rewrite /sd 2![in X in X ≤ _]big_ord_recr
                  [X in _ ≤ X]big_ord_recr /= !addnA.
    apply: leq_add; last first.
      apply: leq_trans (gdist_cunlift _); last by apply: shanoi_connect.
      rewrite leq_eqVlt; apply/orP; left; apply/eqP.
      rewrite !ffunE ![in LHS]inordK //=.
      by congr(`d[↓[u _],↓[u _]]_smove);
         apply/val_eqP; rewrite /= !inordK //= -bE bE1.
    rewrite leq_eqVlt; apply/orP; left; apply/eqP.
    rewrite !big_ord_recr big_ord0 /= !ffunE !inordK //= add0n.
    rewrite -addnA add2n -du0u1.
    move: bE; rewrite -bE1.
    case: (l) u ⇒ // [] [] // uu _; rewrite big_ord_recl big_ord0 addn0 /=.
    by congr(`d[uu _, uu _]_smove); apply/val_eqP; rewrite /= !inordK.
  have cH1 (k : 'I_5) :
    0 < k < 4 → codom (u1 k) \subset [:: p3; a[p1, p2] k].
    case: k ⇒ [] [|[|[|[|]]]] //= iH _; rewrite !ffunE !(apegS, apeg0).
    - by have := s0C; rewrite u1LE.
    - by rewrite codom_subC -KH1.
    rewrite codom_subC.
    apply/subsetP⇒ i /codomP[x ->]; rewrite !ffunE.
    have /cH: 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK //.
    by rewrite inordK // ⇒
        /subsetP /(_ (u (inord 1) (trshift 1 x)) (codom_f _ _)).
  have {cH1}P2 :
     (S_[4] n.+1).*2 ≤ sd u1 + sp (u1 ord0) 4 p1 + sp (u1 ord_max) 4 p1.
    by apply: IH cH1 ⇒ //; rewrite eq_sym.
  set xP := sd _; rewrite -/xP in P1.
  have {}P2 :=
    leq_trans P2 (leq_add (leq_add (leqnn _ ) (leq_sum_beta _ _))
                          (leq_sum_beta _ _)).
  set x1P := sd _ in P1; rewrite -/x1P in P2.
  rewrite !ffunE /= (_ : inord 2 = ord_max) in P2; last first.
    by apply: val_inj; rewrite /= inordK // -bE bE1.
  rewrite {2}(_ : p1 = a[p3, p1] l) in P2; last first.
    by rewrite -bE -bE1.
  set x1S := \sum_(_ < _) _ in P2; set x2S := \sum_(_ < _) _ in P2.
  rewrite !sum_beta_S //= KH1 KH2 !eqxx !addn0 mul1n.
  rewrite -/x1S -/x2S -!addnA.
  apply: leq_trans (leq_add P1 (leqnn _)).
  rewrite -!addnA addnC !addnA -addnA.
  apply: leq_trans (leq_add P2 (leqnn _)).
  rewrite -bE -bE1 -addnn {2}dsum_alphaL_S addnA.
  rewrite [_ + 2]addnC !addnA leq_add2r addnC.
  by apply: leq_dsum_alpha_2l_l 2 n.+1.
have aEl : a = l.+1.
  apply/eqP; rewrite eqn_leq aLld1 /=.
  case/orP: oH; first by case: (a) aD1 a_gt0 ⇒ [|[|]].
  case/orP: o1H; first by case: (a) aD1 a_gt0 ⇒ [|[|]].
  rewrite /b prednK // ⇒ H1 lLa; move: lLa H1.
  by rewrite leq_eqVlt ⇒ /orP[] // /eqP ->; rewrite subSn // subnn eqxx.
have bE0 : b = 0 by rewrite /b aEl subnn.
pose si i : configuration 4 n.+1 :=
  sgdist1 p2 (u (inord i)) (u (inord i.+1)).
pose ti i : configuration 4 n.+1 :=
   sgdist2 p2 (u (inord i)) (u (inord i.+1)).
have sitiH i : i < l →
   [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ],
       codom (ti i) \subset [:: u (inord i) ldisk; p2] &
       `d[u (inord i), u (inord i.+1)]_smove =
         D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2].
  move⇒ iLl.
  have iLl1 : i < l.+1 by rewrite (leq_trans iLl).
  apply: sgdistE ⇒ //.
  - by rewrite aMin1 // aEl.
  - rewrite !aMin1 ?aEl //.
    by rewrite apegS apeg_eqC.
  - by rewrite aMin1 ?aEl // eq_sym.
  - by rewrite aMin1 // aEl.
  by rewrite aMin1 // aEl.
pose u1 :=
  [ffun i ⇒
    if ((i : 'I_(3 × l).+2) == (3 × l).+1 :>nat) then ↓[u ai]
    else if (i %% 3) == 0 then ↓[u (inord (i %/ 3))]
    else if (i %% 3) == 1 then si (i %/ 3)
    else ti (i %/ 3)].
have u10E : u1 ord0 = ↓[u ord0].
  rewrite ffunE /=.
  by congr (↓[u _]); apply/val_eqP; rewrite /= inordK.
have u1mE : u1 ord_max = ↓[u ord_max].
  rewrite ffunE eqxx.
  by congr (↓[u _]); apply/val_eqP/eqP; rewrite /= inordK.
have P1 : l.*2 + sd u1 ≤ sd u.
  rewrite /sd !big_ord_recr /=.
  rewrite addnA; apply: leq_add; last first.
    apply: leq_trans (gdist_cunlift _); last by apply: shanoi_connect.
    rewrite leq_eqVlt; apply/orP; left; apply/eqP.
    rewrite !ffunE !inordK ?eqxx //.
    rewrite eqn_leq [_ ≤ _ × _]leqNgt leqnn andbF mod3E /= div3E.
    congr (`d[↓[u _], ↓[u _]]_smove); apply/val_eqP; rewrite /= ?mulKn //.
    by rewrite inordK // aiE aEl.
  rewrite leq_eqVlt; apply/orP; left; apply/eqP.
  have → := @sum3E _ (fun i ⇒ `d[u1 (inord i), u1 (inord i.+1)]_smove).
  have → : l.*2 = \sum_(i < l) 2.
    by rewrite sum_nat_const /= cardT size_enum_ord muln2.
  rewrite -big_split /=; apply: eq_bigr ⇒ i _.
  rewrite ffunE !inordK //; last first.
    by rewrite ltnS ltnW // ltnS leq_mul2l /= ltnW.
  rewrite eqn_leq [_ ≤ _ × _]leqNgt ltnS leq_mul2l //=.
  rewrite (ltnW (ltn_ord _)) andbF mod3E /= div3E.
  rewrite ffunE !inordK //; last first.
    by rewrite !ltnS leq_mul2l /= ltnW.
  rewrite eqn_leq [_.+1 ≤ _]leqNgt !ltnS leq_mul2l /= [_ ≤ i]leqNgt.
  rewrite ltn_ord andbF mod3E /= div3E -[(_ × _).+3](mulnDr 3 1 i) add1n.
  rewrite ffunE !inordK //; last first.
    by rewrite!ltnS ltn_mul2l /=.
  rewrite !mod3E /= !div3E ifN; last first.
    case: eqP ⇒ // eH.
    have : (3 × i).+2 %% 3 = (3 × l).+1 %% 3 by rewrite eH.
    by rewrite !mod3E.
  rewrite ffunE inordK; last first.
    by rewrite ltnS ltnW // ltnS leq_mul2l /=.
  rewrite mod3E /= div3E ifN.
    case: (sitiH i) ⇒ //= _ _ →.
    by rewrite /= !addnA addn0.
  case: eqP ⇒ // eH.
  have : (3 × i.+1) %% 3 = (3 × l).+1 %% 3 by rewrite eH.
  by rewrite !mod3E.
have cH1 (k : 'I_(3 × l).+2) :
    0 < k < (3 × l).+1 → codom (u1 k) \subset [:: p2; a[p1, p3] k].
  rewrite !ffunE.
  case: eqP ⇒ [->|/eqP kD3l1]; first by rewrite ltnn andbF.
  case: eqP ⇒ [km3E0|/eqP km3D0].
    rewrite {1 2 4}(divn_eq k 3) km3E0 addn0.
    rewrite ltnS mulnC muln_gt0 leq_mul2l /= ⇒ /andP[k3_gt0 k3Ll].
    rewrite apegMr //.
    have:= @H (inord (k %/ 3)); rewrite ffunE inordK //; last first.
      by apply: leq_trans k3Ll _.
    by apply; rewrite k3_gt0.
  case: eqP ⇒ [km3E1|/eqP km3D1].
    rewrite {1 2 4}(divn_eq k 3) km3E1 addn1 !ltnS /= mulnC ltn_mul2l /= ⇒ H1.
    case: (sitiH (k %/ 3)) ⇒ //.
    by rewrite apegS apegMr // aMin1 ?apegS // aEl ltnS.
  have km3E2 : k %% 3 = 2.
    by case: (_ %% _) (ltn_mod k 3) km3D0 km3D1 ⇒ // [] [|[|]].
  rewrite {1 2 4}(divn_eq k 3) km3E2 addn2 /= ltnS ⇒ H1.
  have {}H1 : k %/ 3 < l.
    by rewrite -[_ < _](ltn_mul2r 3) [l × 3]mulnC (leq_ltn_trans _ H1).
  rewrite codom_subC.
  case: (sitiH (k %/ 3)) ⇒ // _.
  rewrite !apegS [_ × 3]mulnC apegMr //.
  by rewrite aMin1 // (leq_trans H1) // aEl.
have {cH1}P2 :
   (S_[(3 × l).+1] n.+1).*2 ≤ sd u1 + sp (u1 ord0) (3 × l).+1 p1 +
                               sp (u1 ord_max) (3 × l).+1
                                               (a[p1, p3] (3 × l).+1).
  by apply: IH cH1.
 have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                          (leq_sum_beta _ _)).
set xP := sd _; rewrite -/xP in P1.
set x1P := sd _ in P1.
rewrite -/x1P (_ : a[p1, p3] (3 × l).+1 = a[p3, p1] l) in P2; last first.
  by rewrite apegS apegMr.
rewrite !sum_beta_S // KH1 KH2 !eqxx addn0 mul1n.
rewrite !ffunE /= eqxx inord_eq0 // (_ : ai = ord_max) in P2; last first.
  by apply: val_inj; rewrite /= inordK.
set x1S := \sum_(_ < _) _ in P2; set x2S := \sum_(_ < _) _ in P2.
rewrite -/x1S -/x2S .
rewrite -addnn {1}dsum_alphaL_S addnAC !addnA leq_add2r.
rewrite -[X in _ ≤ X]addnA.
apply: leq_trans (leq_add P1 (leqnn _)).
rewrite -[X in _ ≤ X]addnA [x1P + _]addnA.
apply: leq_trans (leq_add (leqnn _) P2).
apply: leq_trans (leq_dsum_alpha_2l_l _ _) _.
rewrite addnC; apply: leq_add.
  by rewrite -addnn -addn1 leq_add.
rewrite leq_double.
apply: (increasingE (increasing_dsum_alphaL_l _)).
by rewrite doubleS ltnS -mul2n ltn_mul2r l_ggt0.
Qed.

End Case1.

Section Case2.

Variable n : nat.

Hypothesis IH:
     ∀ (l : nat) (p1 p2 p3 : ordinal_eqType 4)
       (u : {ffun 'I_l.+1 → configuration 4 n.+1}),
     p1 != p2 →
     p1 != p3 →
     p2 != p3 →
     p1 != p0 →
     p2 != p0 →
     p3 != p0 →
     (∀ k : 'I_l.+1,
      0 < k < l → codom (u k) \subset [:: p2; a[p1, p3] k]) →
     (S_[l] n.+1).*2 ≤ sd u + sp (u ord0) l (a[p1, p3] 0) +
                            sp (u ord_max) l (a[p1, p3] l).

Lemma case2 l (u : {ffun 'I_l.+2 → configuration 4 n.+2})
              (p1 p2 p3: peg 4) :
   p1 != p2 → p1 != p3 → p2 != p3 →
   p1 != p0 → p2 != p0 → p3 != p0 →
  (∀ k : 'I_l.+2,
     0 < k < l.+1 → codom (u k) \subset [:: p2; a[p1, p3] k]) →
  (u ord0 ord_max = p1) →
  (u ord_max ord_max = a[p3, p1] l) →
  (∀ k, u k ldisk = a[p1, p3] k) →
  (S_[l.+1] n.+2).*2 ≤ sd u + sp (u ord0) l.+1 p1
                             + sp (u ord_max) l.+1 (a[p3, p1] l).
Proof.
move⇒ p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0.
move⇒ /= cH KH1 KH2 ukLE.
pose u':= ([ffun i ⇒ ↓[u i]] : {ffun 'I_l.+2 → configuration 4 n.+1})
 : {ffun 'I_l.+2 → configuration 4 n.+1}.
have H: ∀ k : 'I_l.+2,
    0 < k < l.+1 → codom (u' k) \subset [:: p2; a[p1, p3] k].
  by move⇒ k kH; rewrite ffunE; apply/codom_liftr/cH.
have apegpaD2 a : a[p1, p3] a != p2.
  by rewrite /apeg; case: odd; rewrite // eq_sym.
have apegpaD0 a : a[p1, p3] a != p0.
  by rewrite /apeg; case: odd; rewrite // eq_sym.
pose si i : configuration 4 n.+1 :=
    sgdist1 p2 (u (inord i)) (u (inord i.+1)).
pose ti i : configuration 4 n.+1 :=
    sgdist2 p2 (u (inord i)) (u (inord i.+1)).
have sitiH i : i < l.+1 →
    [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ],
        codom (ti i) \subset [:: u (inord i) ldisk; p2] &
        `d[u (inord i), u (inord i.+1)]_smove =
          D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2].
  move⇒ iLl.
  have i1Ll1 : i ≤ l by [].
  apply: sgdistE; rewrite ?ukLE //.
    rewrite !inordK //=; last by rewrite ltnS ltnW // ltnS.
    by rewrite apegS apeg_eqC.
  by rewrite eq_sym.
pose u1 :=
  [ffun i ⇒
  if ((i : 'I_(3 × l.+1).+1) %% 3) == 0 then ↓[u (inord (i %/ 3))]
  else if (i %% 3) == 1 then si (i %/ 3)
  else ti (i %/ 3)].
have u10E : u1 ord0 = ↓[u ord0].
  rewrite ffunE /=.
  by congr (↓[u _]); apply/val_eqP; rewrite /= inordK.
have u1ME : u1 ord_max = ↓[u ord_max].
  rewrite ffunE /= mod3E /= div3E.
  by congr (↓[u _]); apply/val_eqP; rewrite /= inordK.
have P1 : l.+1.*2 + sd u1 = sd u.
  rewrite /sd.
  have → := @sum3E _ (fun i ⇒ `d[u1 (inord i), u1 (inord i.+1)]_smove).
  have → : l.+1.*2 = \sum_(i < l.+1) 2.
    by rewrite sum_nat_const /= cardT size_enum_ord muln2.
  rewrite -big_split /=; apply: eq_bigr ⇒ i _.
  rewrite ffunE !inordK //; last first.
    by rewrite ltnS leq_mul2l ltnW.
  rewrite mod3E /= div3E.
  rewrite ffunE inordK; last first.
    by rewrite ltnS ltn_mul2l /=.
  rewrite mod3E /= div3E.
  rewrite ffunE inordK; last first.
    by rewrite -[_.+3](mulnDr 3 1) ltnW // ltnS leq_mul2l /= add1n.
  rewrite mod3E /= div3E.
  rewrite ffunE inordK; last first.
    by rewrite -[(_ × _).+3](mulnDr 3 1) ltnS leq_mul2l /=.
  rewrite -[(_ × _).+3](mulnDr 3 1) mod3E /= div3E.
  case: (sitiH i) ⇒ // _ _.
  by rewrite /= add2n addn0 !addnA add1n.
have cH1 (k : 'I_(3 × l.+1).+1) :
  0 < k < 3 × l.+1 → codom (u1 k) \subset [:: p2; a[p1, p3] k].
  rewrite !ffunE.
  case: eqP ⇒ [km3E0|/eqP km3D0].
    rewrite {1 2 4}(divn_eq k 3) km3E0 addn0.
    rewrite muln_gt0 andbT [_ × 3]mulnC ltn_mul2l /= ⇒ /andP[k3_gt0 k3Ll].
    rewrite apegMr //.
    have:= @H (inord (k %/ 3)); rewrite ffunE inordK //; last first.
      by apply: leq_trans k3Ll _.
    by apply; rewrite k3_gt0.
  case: eqP ⇒ [km3E1|/eqP km3D1].
    rewrite {1 2 4}(divn_eq k 3) km3E1 addn1 /= ⇒ H1.
    have : 3 × (k %/ 3) < 3 × l.+1.
      apply: leq_trans H1; first by rewrite mulnC ltnW.
      rewrite ltn_mul2l /= ⇒ k3Ll1.
    case: (sitiH (k %/ 3)) ⇒ //.
    by rewrite apegS [_ × 3]mulnC apegMr // ukLE inordK // apegS.
  have km3E2 : k %% 3 = 2.
    by case: (_ %% _) (ltn_mod k 3) km3D0 km3D1 ⇒ // [] [|[|]].
  rewrite {1 2 4}(divn_eq k 3) km3E2 addn2 /= -[_.+3](mulnDl 1 _ 3).
  rewrite mulnC leq_mul2l /= add1n ⇒ H1.
  rewrite codom_subC.
  case: (sitiH (k %/ 3)) ⇒ // _ sH _; move: sH.
  by rewrite ukLE // inordK ?(leq_trans H1) // !apegS [_ × 3]mulnC apegMr.
have {cH1}P2 :
    (S_[3 × l.+1] n.+1).*2 ≤ sd u1 + sp (u1 ord0) (3 × l.+1) p1
                                    + sp (u1 ord_max) (3 × l.+1)
                                         (a[p1, p3] (3 × l.+1)).
  by apply: IH cH1.
have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                        (leq_sum_beta _ _)).
rewrite [X in _ ≤ _ + X + _]big_ord_recr /= ukLE eqxx addn0.
rewrite [X in _ ≤ _ + X]big_ord_recr /= ukLE apegS eqxx addn0.
set x1S := \sum_(_ < n.+1) _ in P2; set x2S := \sum_(_ < n.+1) _ in P2.
rewrite [X in _ ≤ _ + X + _](_ : _ = x1S); last first.
  apply: eq_bigr ⇒ i _.
  rewrite u10E ffunE /beta ifF; last first.
    by rewrite eqn_leq [_ ≤ i]leqNgt ltn_ord !andbF.
  by congr ((u _ _ != _) × _); apply/val_eqP; rewrite /=.
rewrite [X in _ ≤ _ + X](_ : _ = x2S); last first.
  apply: eq_bigr ⇒ i _.
  rewrite u1ME ffunE /beta ifF; last first.
    by rewrite eqn_leq [_ ≤ i]leqNgt ltn_ord !andbF.
  congr ((u _ _ != _) × _); first by apply/val_eqP.
  by rewrite apegMr // apegS.
rewrite -P1 -!addnA addnC !addnA.
apply: leq_trans (leq_add P2 (leqnn _)).
by rewrite -doubleD leq_double dsum_alpha3l.
Qed.

End Case2.

Section Case3.

Variable n : nat.

Hypothesis IH:
  ∀ (l : nat) (p1 p2 p3 : ordinal_eqType 4)
    (u : {ffun 'I_l.+1 → configuration 4 n.+1}),
  p1 != p2 →
  p1 != p3 →
  p2 != p3 →
  p1 != p0 →
  p2 != p0 →
  p3 != p0 →
  (∀ k : 'I_l.+1,
  0 < k < l → codom (u k) \subset [:: p2; a[p1, p3] k]) →
  (S_[l] n.+1).*2 ≤ sd u + sp (u ord0) l p1 + sp (u ord_max) l (a[p1, p3] l).

Lemma case3 l (u : {ffun 'I_l.+2 → configuration 4 n.+2})
              (p1 p2 p3: peg 4) :
   p1 != p2 → p1 != p3 → p2 != p3 →
   p1 != p0 → p2 != p0 → p3 != p0 →
  (∀ k : 'I_l.+2,
     0 < k < l.+1 → codom (u k) \subset [:: p2; a[p1, p3] k]) →
  (u ord0 ord_max = p1) →
  (u ord_max ord_max = a[p3, p1] l) →
  (S_[l.+1] n.+2).*2 ≤ sd u + sp (u ord0) l.+1 p1
                             + sp (u ord_max) l.+1 (a[p3, p1] l).
Proof.
move⇒ p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0.
move⇒ cH KH1 KH2.
pose u':= ([ffun i ⇒ ↓[u i]] : {ffun 'I_l.+2 → configuration 4 n.+1})
 : {ffun 'I_l.+2 → configuration 4 n.+1}.
have H: ∀ k : 'I_l.+2,
    0 < k < l.+1 → codom (u' k) \subset [:: p2; a[p1, p3] k].
  by move⇒ k kH; rewrite ffunE; apply/codom_liftr/cH.
have apegpaD2 a : a[p1, p3] a != p2.
  by rewrite /apeg; case: odd; rewrite // eq_sym.
have apegpaD0 a : a[p1, p3] a != p0.
  by rewrite /apeg; case: odd; rewrite // eq_sym.
case: (pickP (fun i ⇒ u i ldisk != a[p1, p3] i)) ⇒ [x xH|pH]; last first.
  have {pH}ukLE k : u k ldisk = a[p1, p3] k by have := pH k; case: eqP.
  have := case2 _ _ _ _ _ _ _ cH KH1 KH2 ukLE.
  by apply.
have exH : ∃ x, u (inord x) ldisk != a[p1, p3] x.
  ∃ x; rewrite (_ : inord x = x) //.
  by apply/val_eqP; rewrite /= inordK.
case: (@ex_minnP _ exH) ⇒ a aH {exH}aMin.
have exL : ∃ x, (x ≤ l) && (u (inord x) ord_max != a[p1, p3] x).
  ∃ x; apply/andP; split ⇒ //.
    have := ltn_ord x.
     rewrite ltnS leq_eqVlt ⇒ /orP[] // /eqP xEl1.
    case/eqP: xH.
    rewrite (_ : x = ord_max); last by apply/val_eqP/eqP.
    by apply/eqP/val_eqP; rewrite /= apegS.
  by rewrite (_ : inord x = x) //; apply/val_eqP; rewrite /= inordK.
have exL1 y : (y ≤ l) && (u (inord y) ord_max != a[p1, p3] y) → y ≤ l.
  by case/andP.
pose a1 := ex_maxn exL exL1.
have a1H: u (inord a1) ldisk != a[p1, p3] a1.
  by rewrite /a1; case: ex_maxnP ⇒ i /andP[].
have a1Ll : a1 ≤ l by rewrite /a1; case: ex_maxnP ⇒ i /andP[].
have a1Max i : a1 < i < l.+2 → u (inord i) ord_max = a[p1, p3] i.
  case/andP⇒ a1Li; rewrite ltnS leq_eqVlt ⇒ /orP[/eqP iEl1|iLl].
    rewrite iEl1 apegS (_ : inord l.+1 = ldisk) //.
    by apply/val_eqP; rewrite /= inordK.
  move: a1Li; rewrite /a1; case: ex_maxnP ⇒ j _ /(_ i).
  by case: eqP; rewrite // andbT ⇒ _ /(_ iLl); rewrite ltnNge ⇒ →.
have aLld1 : a ≤ l.+1.
  rewrite -ltnS; apply: leq_trans (ltn_ord x).
  rewrite ltnS; apply: aMin;rewrite (_ : inord x = x) //.
  by apply/val_eqP; rewrite /= inordK.
wlog aLl1Ba1 : u p1 p3 p1Dp3 p2Dp3 p3Dp0 apegpaD2 apegpaD0 p1Dp2 p1Dp0
   {u' H xH exL exL1}cH KH1 KH2 a a1 aH aLld1 aMin a1H a1Ll a1Max /
  a ≤ l.+1 - a1.
  move⇒ wH.
  case: (leqP a (l.+1 -a1)) ⇒ [aLl1Ba1|l1Ba1La].
    by apply: wH aLl1Ba1.
  have a_gt0 : 0 < a by apply: leq_ltn_trans l1Ba1La.
  pose u1 : {ffun 'I_l.+2 → configuration 4 n.+2} :=
     [ffun i : 'I_l.+2 ⇒ u (inord (l.+1 - i))].
  have → : sd u = sd u1.
    have F : injective (fun i : 'I_l.+1 ⇒ (inord (l - i) : 'I_l.+1)).
      move⇒ i j /val_eqP.
        have lBiLl (i1 : 'I_l.+1) : l - i1 < l.+1.
          by rewrite ltn_subLR ?leq_addl // -ltnS.
      rewrite /= !inordK // ⇒ /eqP liE; apply/val_eqP ⇒ /=.
      rewrite -(subKn (_ : i ≤ l)); last by rewrite -ltnS.
      by rewrite liE subKn // -ltnS.
    rewrite [sd u](reindex_inj F) /=.
    apply: eq_bigr ⇒ i _; rewrite !ffunE.
    have iLl2 : i < l.+2 by apply: leq_trans (ltn_ord _) _.
    have lBiLl : l - i < l.+1 by rewrite ltn_subLR ?leq_addl // -ltnS.
    have iLl : i ≤ l by rewrite -ltnS.
    rewrite gdistC; last by apply/move_sym/ssym.
    congr (`d[u _,u _]_smove).
      by apply/val_eqP; rewrite /= !inordK ?subSn.
    by apply/val_eqP; rewrite /= !inordK // ?subSS ltnS // ltnW.
  pose p1' := a[p1, p3] l; pose p3' := a[p3, p1] l.
  have → : sp (u ord0) l.+1 p1 = sp (u1 ord_max) l.+1 (a[p1', p3'] l).
    apply: eq_bigr ⇒ i _; congr (_ × _).
    rewrite -apegD addnn apegO odd_double /= apegS apeg0.
    by rewrite ffunE subnn inord_eq0.
  have → : sp (u ord_max) l.+1 (a[p3, p1] l) = sp (u1 ord0) l.+1 p3'.
    apply: eq_bigr ⇒ i _; congr (_ × _).
    rewrite ffunE subn0.
    suff → : inord l.+1 = ord_max :> 'I_l.+2 by [].
    by apply/val_eqP; rewrite /= inordK.
  rewrite addnAC.
  have FF : (l.+1 - a1) ≤ l.+1 - (l.+1 - a).
    by rewrite leq_sub2l // leq_subLR addnC -leq_subLR ltnW.
  have a1Ll1 : a1 ≤ l.+1 by rewrite (leq_trans a1Ll).
  apply: wH FF ⇒ //.
  - by rewrite apeg_eqC eq_sym.
  - by rewrite eq_sym apeg_neq // eq_sym.
  - by rewrite apeg_neq // eq_sym.
  - by move⇒ b; rewrite !apeg_neq // eq_sym.
  - by move⇒ b; rewrite !apeg_neq // eq_sym.
  - by rewrite apeg_neq // eq_sym.
  - by rewrite apeg_neq // eq_sym.
  - move⇒ k /andP[kH1 kH2]; rewrite ffunE.
    have F1 : k ≤ l.+1 by apply: ltnW.
    have F2 : l.+1 - k < l.+2.
      by rewrite ltn_subLR // addnS ltnS leq_addl.
    have → : a[p3', p1'] k = a[p1, p3] (inord (l.+1 - k) : 'I_l.+2) .
      rewrite inordK // -apegD -apegS -addnS.
      by rewrite [LHS]apegO [RHS]apegO oddD oddB //= addbC.
    apply: cH; rewrite inordK // subn_gt0 // ltn_subLR // kH2 //=.
    by rewrite addnS ltnS -{1}[l.+1]add1n leq_add2r.
  - rewrite !ffunE /p1' subn0 -[RHS]KH2; congr (u _ _); apply/val_eqP.
    by rewrite /= inordK.
  - by rewrite !ffunE /p1' subnn inord_eq0 // KH1 /p3' -apegD addnn apeg_double.
  - rewrite ffunE inordK //=; last by rewrite ltnS leq_subr.
    rewrite subKn // -apegD apegO oddD oddB //= addbAC !addNb addbb /=.
    by rewrite -oddS -apegO apegS.
  - by rewrite leq_subr.
  - move⇒ k; rewrite ffunE.
    case: leqP ⇒ //; rewrite ltn_subRL addnC -ltn_subRL ⇒ kH.
    have kLl1 : k < l.+1 by rewrite -subn_gt0 (leq_ltn_trans _ kH).
      rewrite inordK; last by rewrite ltnS ltnW.
      have /a1Max→ : a1 < l.+1 - k < l.+2 by rewrite kH /= ltnS leq_subr.
    case/eqP; rewrite -apegD apegO oddB 1?ltnW // -oddD -apegO.
    by rewrite addSn addnC apegS.
  - rewrite ffunE inordK ?ltnS ?leq_subr //.
    rewrite subKn //.
    rewrite -apegD apegO oddD oddB //= !addNb addbAC addbb /=.
    by rewrite -oddS -apegO apegS.
  - by rewrite -[a]prednK // subSS leq_subr.
  move⇒ k /andP[l1BaLk kLl2]; rewrite ffunE.
  rewrite inordK //; apply/eqP; case: eqP ⇒ // /eqP.
  suff → : a[p3', p1'] k = a[p1, p3] (l.+1 - k).
    by move⇒ /aMin; rewrite leqNgt ltn_subLR // addnC -ltn_subLR // l1BaLk.
  by rewrite [RHS]apegO oddB // -oddD -apegO addSn apegS addnC apegD.
pose u':= ([ffun i ⇒ ↓[u i]] : {ffun 'I_l.+2 → configuration 4 n.+1})
 : {ffun 'I_l.+2 → configuration 4 n.+1}.
have H: ∀ k : 'I_l.+2,
    0 < k < l.+1 → codom (u' k) \subset [:: p2; a[p1, p3] k].
  by move⇒ k kH; rewrite ffunE; apply/codom_liftr/cH.
have aMin1 i : i < a → u (inord i) ord_max = a[p1, p3] i.
  by case: (u (inord i) ord_max =P a[p1, p3] i) ⇒ // /eqP /aMin; case: leqP.
have a_gt0 : 0 < a.
  have : 0 ≤ a by [].
  rewrite leq_eqVlt ⇒ /orP[/eqP aE0|] //.
  by case/eqP: aH; rewrite inord_eq0 // -aE0.
pose ai : 'I_l.+2 := inord a.
have aiE : ai = a :> nat by rewrite inordK.
have aLa1 : a ≤ a1.
  case: leqP ⇒ // ⇒ a1La.
  by case/eqP: aH; apply: a1Max; rewrite a1La.
have uaLEp2 : u (inord a) ldisk = p2.
  have /cH : 0 < (inord a : 'I_l.+2) < l.+1.
    by rewrite inordK // a_gt0 /= (leq_ltn_trans _ (_ : a1 < l.+1)).
  move⇒ /subsetP/(_ (u (inord a) ldisk) (codom_f _ _)).
  by rewrite !inE inordK // (negPf aH) orbF ⇒ /eqP.
have ua1LEp2 : u (inord a1) ldisk = p2.
  have /cH : 0 < (inord a1 : 'I_l.+2) < l.+1.
    by rewrite inordK // !ltnS (leq_trans a1Ll) // (leq_trans a_gt0).
  move⇒ /subsetP/(_ (u (inord a1) ldisk) (codom_f _ _)).
  by rewrite !inE inordK ?ltnS ?(leq_trans a1Ll) // (negPf a1H) orbF ⇒ /eqP.
have a1_gt0 : 0 < a1 by apply: leq_trans a_gt0 _.
pose b := a1 - a.
pose c := l.+1 - a1.
have c_gt0 : 0 < c by rewrite subn_gt0.
have l1E : l.+1 = a + b + c.
  by rewrite /b /c [a + _]addnC subnK // addnC subnK // ltnW.
pose si i : configuration 4 n.+1 :=
   sgdist1 p2 (u (inord i)) (u (inord i.+1)).
pose ti i : configuration 4 n.+1 :=
   sgdist2 p2 (u (inord i)) (u (inord i.+1)).
have sitiH i : i < a.-1 →
   [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ],
       codom (ti i) \subset [:: u (inord i) ldisk; p2] &
       `d[u (inord i), u (inord i.+1)]_smove =
         D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2].
  move⇒ iLa.
  have iLa1 : i < a by rewrite (leq_trans iLa) // ssrnat.leq_pred.
  apply: sgdistE; rewrite ?aMin1 // -1?[a]prednK //.
    by rewrite apegS apeg_eqC.
  by rewrite eq_sym.
pose pa := a[p1, p3] a.
pose sam1 : configuration 4 n.+1 := sgdist1 pa (u (inord a.-1)) (u (inord a)).
pose tam1 : configuration 4 n.+1 := sgdist2 pa (u (inord a.-1)) (u (inord a)).
have [sam1C tam1C duam1ua1E] :
   [/\ codom sam1 \subset [:: pa; u (inord a) ldisk ],
       codom tam1 \subset [:: u (inord a.-1) ldisk; pa] &
       `d[u (inord a.-1), u (inord a)]_smove =
         D[[:: ↓[u (inord a.-1)]; sam1; tam1; ↓[u (inord a)]]].+2].
  apply: sgdistE; rewrite /pa ?uaLEp2 ?aMin1 ?prednK //.
  by rewrite -{2}(prednK a_gt0) apegS apeg_eqC.
rewrite uaLEp2 in sam1C.
have {}tam1C : codom tam1 \subset [:: p1; p3].
  move: tam1C; rewrite aMin1; last by rewrite -{2}[a]prednK.
  by rewrite /pa -{2}[a]prednK // apegS codom_apeg.
pose u1 :=
  [ffun i : 'I_(3 × a).+1 ⇒
  if (i %% 3) == 0 then ↓[u (inord (i %/ 3))]
  else if (i %% 3) == 1 then
     (if i == (3 × a.-1).+1 :> nat then sam1 else si (i %/ 3))
  else
     (if i == (3 × a.-1).+2 :> nat then tam1 else ti (i %/ 3))].
have u10E : u1 ord0 = ↓[u ord0] by rewrite ffunE /= inord_eq0.
have uiME : u1 ord_max = ↓[u (inord a)] by rewrite ffunE /= mod3E /= div3E.
have P1 : a.*2 + sd u1 = \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove.
  rewrite /sd.
  have → := @sum3E _ (fun i ⇒ `d[u1 (inord i), u1 (inord i.+1)]_smove).
  have → : a.*2 = \sum_(i < a) 2.
    by rewrite sum_nat_const /= cardT size_enum_ord muln2.
  rewrite -big_split /=.
  apply: eq_bigr ⇒ i _.
  have → : u1 (inord (3 × i)) = ↓[u (inord i)].
    rewrite ffunE inordK; last by rewrite ltnS leq_mul2l /= ltnW.
    by rewrite mod3E /= div3E.
  have → : u1 (inord (3 × i).+3) = ↓[u (inord i.+1)].
    rewrite -[(_ × _).+3](mulnDr 3 1).
    rewrite ffunE inordK; last by rewrite ltnS leq_mul2l /=.
    by rewrite mod3E /= div3E.
  have [/eqP iEa| iDa] := boolP (i == a.-1 :> nat).
    have → : u1 (inord (3 × i).+1) = sam1.
      rewrite ffunE inordK; last by rewrite ltnS ltn_mul2l /=.
      rewrite mod3E /= div3E.
      by rewrite iEa eqxx.
    have → : u1 (inord (3 × i).+2) = tam1.
      rewrite ffunE inordK; last first.
        by rewrite -[_.+3](mulnDr 3 1) ltnW // add1n ltnS leq_mul2l /=.
      rewrite mod3E /= div3E.
      by rewrite iEa eqxx.
    by rewrite iEa prednK // duam1ua1E /= -!addnA add2n !addnA addn0.
  have → : u1 (inord (3 × i).+1) = si i.
    rewrite ffunE inordK; last by rewrite ltnS ltn_mul2l /=.
    rewrite mod3E /= div3E.
    by rewrite [_.+1 == _.+1]eqn_mul2l /= (negPf iDa).
  have → : u1 (inord (3 × i).+2) = ti i.
    rewrite ffunE inordK; last first.
      by rewrite -[_.+3](mulnDr 3 1) ltnW // ltnS add1n leq_mul2l /=.
    rewrite mod3E /= div3E.
    by rewrite [_.+1 == _.+1]eqn_mul2l /= (negPf iDa).
  case: (sitiH i) ⇒ // [|_ _ ->].
    rewrite -ltnS prednK //.
    have := ltn_ord i; rewrite leq_eqVlt ⇒ /orP[] //.
    by rewrite -{2}[a]prednK // [_ == _](negPf iDa).
  by rewrite /= -!addnA add2n addn0.
have sitiHb i : a1 < i < l.+1 →
   [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ],
       codom (ti i) \subset [:: u (inord i) ldisk; p2] &
       `d[u (inord i), u (inord i.+1)]_smove =
         D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2].
  move⇒ /andP[a1Li iLl].
  apply: sgdistE ⇒ //;
      rewrite !a1Max ?a1Li ?(leq_trans a1Li) // ?(leq_trans iLl) //.
    by rewrite apegS apeg_eqC.
  by rewrite eq_sym.
pose sa1 : configuration 4 n.+1 :=
  sgdist1 (a[p1, p3] a1) (u (inord a1)) (u (inord a1.+1)).
pose ta1 : configuration 4 n.+1 :=
  sgdist2 (a[p1, p3] a1) (u (inord a1)) (u (inord a1.+1)).
have [sa1C ta1C dua1uad1E] :
   [/\ codom sa1 \subset [:: a[p1, p3] a1; u (inord a1.+1) ldisk ],
       codom ta1 \subset [:: u (inord a1) ldisk; a[p1, p3] a1] &
       `d[u (inord a1), u (inord a1.+1)]_smove =
         D[[:: ↓[u (inord a1)]; sa1 ; ta1; ↓[u (inord a1.+1)]]].+2].
  apply: sgdistE; rewrite ?ua1LEp2 ?a1Max ?leqnn // 1?eq_sym //.
  by rewrite apegS apeg_eqC eq_sym.
rewrite ua1LEp2 in ta1C.
have {}sa1C : codom sa1 \subset [:: p1; p3].
  move: sa1C; rewrite a1Max //; last by rewrite leqnn.
  by rewrite apegS codom_apeg.
pose u2 :=
  [ffun i : 'I_(3 × c).+1 ⇒
  if (i %% 3) == 0 then ↓[u (inord (a1 +(i %/ 3)))]
  else if (i %% 3) == 1 then
     (if i == 1 :> nat then sa1 else si (a1 + (i %/ 3)))
  else
     (if i == 2 :> nat then ta1 else ti (a1 + (i %/ 3)))].
have u20E : u2 ord0 = ↓[u (inord a1)] by rewrite ffunE /= addn0.
have u2ME : u2 ord_max = ↓[u ord_max].
  rewrite ffunE /= mod3E /= div3E addnC subnK //.
    by rewrite (_ : inord _ = ord_max) //; apply/val_eqP; rewrite /= inordK.
  by rewrite ltnW // ltnS.
have P2 : c.*2 + sd u2 =
  \sum_(a1 ≤ i < l.+1) `d[u (inord i), u (inord i.+1)]_smove.
  have → : \sum_(a1 ≤ i < l.+1) `d[u (inord i), u (inord i.+1)]_smove =
            \sum_(i < c) `d[u (inord (a1 + i)), u (inord (a1 + i).+1)]_smove.
    rewrite -{1}[a1]add0n big_addn big_mkord.
    by apply: eq_bigr ⇒ i _; rewrite addnC.
  rewrite /sd.
  have → := @sum3E _ (fun i ⇒ `d[u2 (inord i), u2 (inord i.+1)]_smove).
  have → : c.*2 = \sum_(i < c) 2.
    by rewrite sum_nat_const /= cardT size_enum_ord muln2.
  rewrite -big_split /=.
  apply: eq_bigr ⇒ i _.
  have → : u2 (inord (3 × i)) = ↓[u (inord (a1 + i))].
    rewrite ffunE inordK; last by rewrite ltnS leq_mul2l /= ltnW.
    by rewrite mod3E /= div3E.
  have → : u2 (inord (3 × i).+3) = ↓[u (inord (a1 + i).+1)].
    rewrite -[(_ × _).+3](mulnDr 3 1).
    rewrite ffunE inordK; last by rewrite ltnS leq_mul2l /=.
    by rewrite mod3E /= div3E // add1n addnS.
  have [/eqP iEa| iDa] := boolP (i == 0 :> nat).
    have → : u2 (inord (3 × i).+1) = sa1.
      rewrite ffunE inordK; last by rewrite ltnS ltn_mul2l /=.
      rewrite mod3E /=.
      by rewrite iEa eqxx.
    have → : u2 (inord (3 × i).+2) = ta1.
      rewrite ffunE inordK; last first.
        by rewrite -[_.+3](mulnDr 3 1) ltnW // add1n ltnS leq_mul2l /=.
      rewrite mod3E /=.
      by rewrite iEa eqxx.
    by rewrite iEa !addn0 // dua1uad1E /= -!addnA add2n !addnA addn0.
  have → : u2 (inord (3 × i).+1) = si (a1 + i).
    rewrite ffunE inordK; last by rewrite ltnS ltn_mul2l /=.
    rewrite mod3E /= div3E.
    by rewrite [_.+1 == _.+1](eqn_mul2l 3 _ 0) /= (negPf iDa).
  have → : u2 (inord (3 × i).+2) = ti (a1 + i).
    rewrite ffunE inordK; last first.
      by rewrite -[_.+3](mulnDr 3 1) ltnW // ltnS add1n leq_mul2l /=.
    rewrite mod3E /= div3E.
    by rewrite [_.+1 == _.+1](eqn_mul2l 3 _ 0) /= (negPf iDa).
  case: (sitiHb (a1 + i)) ⇒ // [|_ _ ->].
    rewrite -addn1 leq_add2l lt0n iDa /= -[l.+1](subnK (_ : a1 ≤ l.+1)).
      by rewrite addnC ltn_add2r.
    by rewrite ltnW.
  by rewrite /= -!addnA add2n addn0.
have P3 :
     \sum_(a ≤ i < a1) `d[↓[u (inord i)], ↓[u (inord i.+1)]]_smove ≤
     \sum_(a ≤ i < a1) `d[u (inord i), u (inord i.+1)]_smove.
  apply: leq_sum ⇒ i _.
  by apply: gdist_cunlift; apply: shanoi_connect.
have SH : 2 ≤ l →
  (S_[l.+1] n.+2).*2 ≤ S_[l.+1] n.+2 + S_[l] n.+1 + (α_[1] n.+1).*2.
  move⇒ l_gt2.
  rewrite -addnn -!addnA leq_add2l.
  by apply: dsum_alphaL_alpha.
have [/andP[a_gt1 c_gt1]|] := boolP ((1 < a) && (1 < c)).
  have l_gt0 : 0 < l by rewrite -ltnS l1E (leq_trans c_gt1) // leq_addl.
  rewrite !sum_beta_S //= KH1 KH2 !eqxx !addn0.
  pose u1l := [ffun i : 'I_(3 × a).-2.+1 ⇒ u1 (inord i)].
  have a3_gt1 : 1 < (3 × a).-2 by rewrite -(subnK a_gt1) addn2 !mulnS.
  have c3_gt1 : 1 < (3 × c).-2 by rewrite -(subnK c_gt1) addn2 !mulnS.
  have cH1 (k : 'I_(3 × a).-2.+1) :
    0 < k < (3 × a).-2 → codom (u1l k) \subset [:: p2; a[p1, p3] k].
    move⇒ /andP[k_gt0 k3L3a].
    have k3La1 : k %/ 3 ≤ a.-1.
      have kL3a : k ≤ 3 × (a.-1).
        rewrite -[a.-1]subn1 mulnBr -ltnS -[3 ×1]/(2.+1) subnSK.
          by rewrite subn2.
        by rewrite (leq_mul2l 3 1).
      by rewrite -[a.-1](mulKn _ (_ : 0 < 3)) // leq_div2r.
    have k3Ll : k %/ 3 < l.
      rewrite -ltnS l1E (leq_trans (_ : _ < a.-1.+3)) //; last first.
        rewrite prednK // addnAC -addn2 (leq_trans (_ : _ ≤ a + c)) //.
          by rewrite leq_add2l.
        by rewrite leq_addr.
      by rewrite !ltnS ltnW // ltnS.
    rewrite !ffunE inordK //; last first.
      rewrite (leq_trans (ltn_ord _)) // -subn2 ltn_subLR.
        by rewrite add2n ltnS // ltnW.
      by rewrite (leq_trans (_ : _ < 3 × 1)) // leq_mul2l.
    rewrite {8}(divn_eq k 3) apegD [_ × 3]mulnC apegMr //=.
    case: eqP ⇒ [km3E0 /= |/eqP km3D0].
      have k3_gt0 : 0 < k %/ 3.
        case: (k: nat) k_gt0 km3E0 ⇒ // [] [|[|k1 _ _]] //.
        by rewrite (divnMDl 1 k1 (_ : 0 < 3)).
      rewrite km3E0 !apeg0.
      have /H : 0 < (inord (k %/ 3) : 'I_l.+2) < l.+1.
        rewrite inordK //.
          by rewrite k3_gt0 /= (leq_trans k3Ll).
        by rewrite (leq_trans k3Ll) // ltnW.
      by rewrite ffunE inordK // (leq_trans k3Ll) // ltnW .
    case: eqP ⇒ [km3E1|/eqP km3D1].
      rewrite km3E1 !apegS !apeg0; case: eqP ⇒ [->|kE3a1].
        rewrite (_ : (3 × a.-1).+1 = a.-1 × 3 + 1); last by rewrite addn1 mulnC.
        rewrite divnMDl // divn_small // addn0.
        by have := sam1C; rewrite codom_subC /pa -{1}[a]prednK //= apegS.
      move: k3La1; rewrite leq_eqVlt ⇒ /orP[/eqP k3Ea1| k3La].
        case: kE3a1.
        by rewrite (divn_eq k 3) km3E1 k3Ea1 mulnC addn1.
      case: (sitiH (k %/ 3)) ⇒ // siH _ _; move: siH.
      by rewrite aMin1 ?apegS // -{2}[a]prednK .
    have km3E2 : k %% 3 = 2.
      by case: (_ %% _) (ltn_mod k 3) km3D0 km3D1 ⇒ // [] [|[|]].
    rewrite km3E2 !apegS !apeg0; case: eqP ⇒ [kE3a1|kD3a1].
      rewrite ltnNge in k3L3a; case/negP: k3L3a.
      by rewrite kE3a1 -{1}[a]prednK // mulnS.
    move: k3La1; rewrite leq_eqVlt ⇒ /orP[/eqP k3Ea1| k3La].
      case: kD3a1.
      by rewrite (divn_eq k 3) km3E2 k3Ea1 mulnC addn2.
    rewrite codom_subC.
    case: (sitiH (k %/ 3)) ⇒ // _ tiH _; move: tiH.
    by rewrite aMin1 // -{2}[a]prednK // ltnS ltnW.
    have {cH1}P4 :
      (S_[(3 × a).-2] n.+1).*2 ≤
      \sum_(i < (3 × a).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove +
      \sum_(k < n.+1) (↓[u ord0] k != p1) × β_[n.+1, (3 × a).-2] k +
      \sum_(k < n.+1) (sam1 k != pa) × β_[n.+1, (3 × a).-2] k.
    apply: leq_trans (IH _ _ _ _ _ _ cH1) _ ⇒ //.
    rewrite leq_eqVlt; apply/orP; left; apply/eqP.
    congr (_ + _ + _); apply: eq_bigr ⇒ i _.
    - by rewrite ![u1l _]ffunE !inordK // ltnS // ltnW.
    - by rewrite ffunE inord_eq0 // ffunE /= inord_eq0.
    rewrite !ffunE /= inordK //; last first.
      by rewrite ltnS -subn2 leq_subr.
    rewrite (_ : _.-2 = (3 × a.-1).+1); last first.
      by rewrite -{1}[a]prednK // mulnS.
    rewrite mod3E /= eqxx.
    by rewrite /pa apegS apegMr //= -apegS prednK.
  have {}P4 := leq_trans P4 (leq_add (leq_add (leqnn _)
                     (leq_sum_beta _ _)) (leqnn _)).
  set x1S := \sum_(_ < _.+1) _ in P4; set x2S := \sum_(_ < _.+1) _ in P4.
  rewrite -/x1S.
  pose u2r := [ffun i : 'I_(3 × c).-2.+1 ⇒ u2 (inord i.+2)].
  pose pa1 := a[p1, p3] a1.
  pose pa1S := a[p1, p3] a1.+1.
  have cH1 (k : 'I_(3 × c).-2.+1) :
    0 < k < (3 × c).-2 → codom (u2r k) \subset [:: p2; a[pa1, pa1S] k].
    move⇒ /andP[k_gt0 k3L3a].
    have k2L3c : k.+2 < (3 × c).
      by have := k3L3a; rewrite -{2}subn2 ltn_subRL add2n.
    rewrite !ffunE inordK ?ltnS 1?ltnW //.
    case: eqP ⇒ [km3E0 /= |/eqP km3D0].
      have k3_gt0 : 0 < k.+2 %/ 3.
        case: (k: nat) k_gt0 km3E0 ⇒ // [] //= k1 _ _.
        by rewrite (divnMDl 1 k1 (_ : 0 < 3)).
      have a1k3Ll1 : a1 + k.+2 %/ 3 < l.+1.
        move: k2L3c.
        rewrite {1}(divn_eq k.+2 3) km3E0 addn0 mulnC ltn_mul2l /= ⇒ k2L3c.
        rewrite -(subnK (_ : a1 ≤ l.+1)) ?(leq_trans a1Ll) //.
        by rewrite addnC ltn_add2r -/c.
      rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2 %/ 3)) ; last first.
        rewrite /pa1 /pa1S apegS -apegD -2!apegS -!addSn addnC.
        rewrite {1}(divn_eq k.+2 3) km3E0 addn0 apegO.
        by rewrite oddD odd_mul andbT -oddD -apegO.
      have /H : 0 < (inord (a1 + k.+2 %/ 3) : 'I_l.+2) < l.+1.
        rewrite inordK; first by rewrite addn_gt0 a1_gt0.
        by rewrite ltnS ltnW.
      by rewrite ffunE inordK // ltnS ltnW.
    case: eqP ⇒ [km3E1|/eqP km3D1].
      rewrite eqn_leq ltnNge /=.
      have a1La1k : a1 < a1 + k.+2 %/3.
        by rewrite -{1}(addn0 a1) ltn_add2l divn_gt0.
      have a1k3Ll : a1 + k.+2 %/ 3 < l.+1.
        move: (ltnW k2L3c).
        rewrite {1}(divn_eq k.+2 3) km3E1 addn1 mulnC ltn_mul2l /=.
        rewrite -(subnK (_ : a1 ≤ l.+1)) ?(leq_trans a1Ll) //.
        by rewrite addnC ltn_add2r -/c.
      rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first.
        by rewrite /pa1S apegS -apegD !addnS addnC !apegS.
      rewrite (_ : a[_, _ ] _ = a[p3, p1] (a1 + (k.+2) %/ 3)) ; last first.
        rewrite apegO oddD {1}(divn_eq k.+2 3) oddD km3E1 addbT odd_mul andbT.
        by rewrite addbN -oddD -oddS -apegO apegS.
      case: (sitiHb (a1 + k.+2 %/ 3)) ⇒ // [| siH _ _].
        by rewrite a1La1k.
      by move: siH; rewrite a1Max ?apegS // ltnS ltnW.
    have km3E2 : k.+2 %% 3 = 2.
      by case: (_ %% _) (ltn_mod k.+2 3) km3D0 km3D1 ⇒ // [] [|[|]].
    rewrite ifN; last by case: (k : nat) k_gt0.
    have a1La1k : a1 < a1 + k.+2 %/3.
      by rewrite -{1}(addn0 a1) ltn_add2l divn_gt0.
    have a1k3Ll : a1 + k.+2 %/ 3 < l.+1.
      have: k.+2 %/ 3 × 3 < 3 × c.
        rewrite ltnW //.
        move: (ltnW k2L3c).
        by rewrite {1}(divn_eq k.+2 3) km3E2 addn2.
      rewrite mulnC ltn_mul2l /=.
      rewrite -(subnK (_ : a1 ≤ l.+1)) ?(leq_trans a1Ll) //.
      by rewrite addnC ltn_add2r -/c.
    rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first.
      by rewrite /pa1 /pa1S apegS -apegD addnC !addnS !apegS.
    rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + (k.+2) %/ 3)) ; last first.
      rewrite apegO /= oddD {1}(divn_eq k.+2 3) !oddD odd_mul andbT.
      by rewrite km3E2 addbF -oddD -apegO.
    rewrite codom_subC.
    case: (sitiHb (a1 + k.+2 %/ 3)) ⇒ // [| _ tiH _]; first by rewrite a1La1k.
    by move: tiH; rewrite a1Max // a1La1k ltnS ltnW.
  have P5 :
    (S_[(3 × c).-2] n.+1).*2 ≤
    \sum_(i < (3 × c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove +
    sp ta1 (3 × c).-2 pa1 + sp ↓[u ord_max] (3 × c).-2 (a[p3, p1] l).
    apply: leq_trans (IH _ _ _ _ _ _ cH1) _; rewrite /pa1 /pa1S {cH1}//.
    - by rewrite apegS apeg_eqC.
    - by rewrite eq_sym.
    repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.
    - apply: eq_bigr ⇒ i _.
      by rewrite ![u2r _]ffunE !inordK // ltnS // ltnW.
    - apply: eq_bigr ⇒ i _; congr ((_ != _) × _).
      rewrite !ffunE /= !inordK //=.
      by rewrite (leq_trans (_ : 2 < (3 × 1).+1)) // ltnS leq_mul2l.
    apply: eq_bigr ⇒ i _; congr ((_ != _) × _).
      rewrite !ffunE /= !prednK ?muln_gt0 //=; last first.
        by rewrite -subn1 ltn_subRL addn0 (leq_trans (_ : _ < 3 × 1)) //
                   leq_mul2l.
      rewrite inordK // mod3E /= div3E addnC subnK; last first.
        by apply: (leq_trans a1Ll).
      by rewrite ffunE; congr (u _ _ ); apply/val_eqP; rewrite /= inordK.
    rewrite -[RHS]apegS -(subnK (_ : a1 ≤ l.+1)) // -/c.
      rewrite apegS -apegD apegO oddD -subn2 oddB.
        by rewrite addbF odd_mul /= -oddD -apegO.
      by rewrite (leq_trans (_ : _ < 3 × 1)) // leq_mul2l //.
    by rewrite ltnW.
  rewrite {cH1}//.
  have {}P5 :=
    leq_trans P5 (leq_add (leqnn _) (leq_sum_beta _ _)).
  set y1S := \sum_(_ < _) _ in P5; set y2S := sp _ _ _ in P5.
  have [b_gt1|b_le2] := leqP 2 b.
    pose u3 := [ffun i : 'I_3 ⇒
                 if i == 0 :> nat then sam1
                 else if i == 1 :> nat then tam1 else ↓[u (inord a)]].
    have cH6 (k : 'I_3) :
      0 < k < 2 → codom (u3 k) \subset [:: p1; a[p2, p3] k].
      move⇒ /andP[k_gt0 k_lt2].
      rewrite !ffunE.
      by have ->/= : k = 1 :> nat by case: (k : nat) k_gt0 k_lt2 ⇒ // [] [|].
    have P6 :
      (S_[2] n.+1).*2 ≤
      (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove) + sp sam1 2 p2
                                                + sp ↓[u (inord a)] 2 p2.
      apply: (leq_trans (IH _ _ _ _ _ _ cH6)) ⇒ //.
        by rewrite eq_sym.
      repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.
      - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /=.
      - by apply: eq_bigr ⇒ i _; rewrite !ffunE.
      by apply: eq_bigr ⇒ i _; rewrite !ffunE.
    rewrite {cH6}// in P6.
    set x3S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6.
    have x2Sx3SE : x2S + x3S ≤ (S_[1] n).*2 + α_[maxn (3 × a).-2 2] n.
      by apply: sum_alpha_diffE; by rewrite /pa.
    rewrite (maxn_idPl _) // in x2Sx3SE.
    pose u4 := [ffun i : 'I_b.+1 ⇒ ↓[u (inord (a + i))]].
    pose paS := a[p1, p3] a.+1.
    have cH7 (k : 'I_b.+1) :
      0 < k < b → codom (u4 k) \subset [:: p2; a[pa, paS] k].
      move⇒ /andP[k_gt0 k_ltb].
      have akLl : a + k < l.+1.
        rewrite ltnS (leq_trans _ a1Ll) //.
        by rewrite -(subnK aLa1) addnC leq_add2r ltnW.
      rewrite !ffunE.
      have /H : 0 < (inord (a + k) : 'I_l.+2) < l.+1.
        rewrite inordK; first by rewrite addn_gt0 a_gt0.
        by rewrite ltnS ltnW.
      rewrite ffunE inordK //; last by rewrite ltnS ltnW.
      by rewrite /pa /paS apegS -apegD [k + _]addnC.
    have P7 :
      (S_[b] n.+1).*2 ≤
      \sum_(i < b) `d[↓[u (inord (a + i))], ↓[u (inord (a + i).+1)]]_smove +
      sp ↓[u (inord a)] b pa + sp ↓[u (inord a1)] b (a[p1, p3] a1).
      apply: leq_trans (IH _ _ _ _ _ _ cH7) (leq_add (leq_add _ _) _);
        rewrite /pa /paS // 1?eq_sym //.
      - by rewrite apegS apeg_eqC eq_sym.
      - apply: leq_sum ⇒ i; rewrite !ffunE !inordK ?addnS //.
          by rewrite ltnS.
        by rewrite ltnS ltnW.
      - by apply: leq_sum ⇒ i _; rewrite !ffunE addn0.
      apply: leq_sum ⇒ i _; rewrite !ffunE /= [a + b]addnC subnK //.
      by rewrite apegS -apegD subnK.
    set x4S := sp _ _ _ in P7; set y4S := sp _ _ _ in P7.
    have y3Sx4SE : y3S + x4S ≤ (S_[1] n).*2 + α_[maxn 2 b] n.
      apply: sum_alpha_diffE ⇒ //; first by rewrite /pa eq_sym.
      apply: codom_liftr.
      have := @cH (inord a); rewrite inordK //; apply.
      by rewrite a_gt0 /= ltnS (leq_trans _ a1Ll).
    rewrite (maxn_idPr _) // in y3Sx4SE.
    pose u5 := [ffun i : 'I_3 ⇒
                     if i == 0 :> nat then ↓[u (inord a1)]
                 else if i == 1 :> nat then sa1 else ta1].
    have cH8 (k : 'I_3) :
      0 < k < 2 → codom (u5 k) \subset [:: p1; a[p2, p3] k].
      move⇒ /andP[k_gt0 k_lt2].
      rewrite !ffunE.
      by have ->/= : k = 1 :> nat by case: (k : nat) k_gt0 k_lt2 ⇒ // [] [|].
    have P8 :
      (S_[2] n.+1).*2 ≤
      (`d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove) +
        sp ↓[u (inord a1)] 2 p2 + sp ta1 2 p2.
      apply: (leq_trans (IH _ _ _ _ _ _ cH8)) ⇒ //; first by rewrite eq_sym.
      repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.
      - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /=.
      - by apply: eq_bigr ⇒ i _; rewrite !ffunE.
      by apply: eq_bigr ⇒ i _; rewrite !ffunE.
    set x5S := sp _ _ _ in P8; set y5S := sp _ _ _ in P8.
    have y4Sx5SE : y4S + x5S ≤ (S_[1] n).*2 + α_[maxn b 2] n.
      apply: sum_alpha_diffE ⇒ //.
      apply: codom_liftr; rewrite codom_subC.
      have := @cH (inord a1); rewrite inordK //.
        by apply; rewrite a1_gt0 /= ltnS.
      by rewrite ltnS ltnW.
    rewrite (maxn_idPl _) // in y4Sx5SE.
    have y2Sy5SE : y2S + y5S ≤ (S_[1] n).*2 + α_[maxn (3 × c).-2 2] n.
      apply: sum_alpha_diffE ⇒ //; first by rewrite /pa1.
      by rewrite codom_subC.
    rewrite (maxn_idPl _) // in y2Sy5SE.
    rewrite (_ : sd u =
       \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove +
       \sum_(a ≤ i < a1) `d[u (inord i), u (inord i.+1)]_smove +
       \sum_(a1 ≤ i < l.+1) `d[u (inord i), u (inord i.+1)]_smove); last first.
      pose f i := `d[u (inord i), u (inord i.+1)]_smove.
      rewrite /sd -!(big_mkord xpredT f).
      by rewrite -!big_cat_nat //= ltnW.
    rewrite -{}P1 -{}P2.
    rewrite [X in _ ≤ _ + X + _ + _ + _ + _]
       (_ : _ =
              \sum_(i < (3 × a).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove
              + `d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove);
              last first.
      pose f i := `d[u1 (inord i), u1 (inord i.+1)]_smove.
      rewrite /sd -!(big_mkord xpredT f) .
      rewrite -{1}(subnK (_ : 1 < 3 × a)) //; last first.
        by rewrite -[a]prednK // mulnS.
      rewrite subn2 !addn2 !big_nat_recr /f //=; congr (_ + _ + _).
        rewrite ffunE (_ : (3 × a).-2 = (3 × (a.-1)).+1); last first.
          by rewrite -{1}[a]prednK // mulnS.
        rewrite inordK; last by rewrite ltnS ltn_mul2l /= prednK.
        rewrite mod3E /= eqxx.
        rewrite ffunE inordK; last first.
          by rewrite -[_.+3](mulnDr 3 1) add1n prednK // ltnW.
        by rewrite mod3E /= eqxx.
      rewrite ffunE (_ : (3 × a).-2 = (3 × (a.-1)).+1); last first.
        by rewrite -{1}[a]prednK // mulnS.
      rewrite inordK; last first.
        by rewrite -{2}[a]prednK // mulnS.
      rewrite mod3E /= eqxx.
      rewrite ffunE inordK; last first.
        by rewrite -{2}[a]prednK // mulnS.
      by rewrite -[(_ × _).+3](mulnDr 3 1) mod3E /= div3E add1n prednK.
    rewrite [X in _ ≤ _ + (_ + X) + _ + _]
       (_ : _ = `d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove +
         \sum_(i < (3 × c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove);
        last first.
      pose f i := `d[u2 (inord i), u2 (inord i.+1)]_smove.
      rewrite /sd -!(big_mkord xpredT f) .
      rewrite -{1}(subnK (_ : 1 < 3 × c)) //; last first.
        by rewrite -[c]prednK // mulnS.
      rewrite subn2 !addn2 !big_nat_recl // /f /= !addnA; congr (_ + _ + _).
      - rewrite !ffunE !inordK ?addn0 //=.
        by rewrite ltnS muln_gt0.
      - rewrite !ffunE !inordK //=.
          by rewrite ltnW // ltnS (leq_mul2l 3 1 c).
        by rewrite ltnS muln_gt0.
      by rewrite big_mkord.
    rewrite -/y1S.
    set z1S := \sum_(_ < _) _; set z2S := \sum_(_ < _) _.
    set z3S := \sum_(_ ≤ _ < _) _.
    rewrite -/z1S in P4; rewrite -/z2S in P5; rewrite -/z3S in P3.
    rewrite -[z1S + _ + _]addnA; set d1 := `d[_,_]_ _ + `d[_,_]_ _;
       rewrite -/d1 in P6.
    set d2 := `d[_,_]_ _ + `d[_,_]_ _; rewrite -/d2 in P8.
    set xS := \sum_(_ ≤ _ < _) _ in P3.
    rewrite [X in _ ≤ X + _ + _](_ : _ = xS) in P7; last first.
      rewrite /xS -[in RHS](add0n a) big_addn -/b big_mkord.
      by apply: eq_bigr ⇒ i _; rewrite [a + _]addnC.
    have F1 := dsum_alphaL_S (3 × a).-2 n.
    have F2 := dsum_alphaL_S (3 × c).-2 n.
    have F3 := dsum_alphaL_S b n.
    have F4_a : 2 × a = 2 + a.-1 + a.-1.
      by rewrite -{1}[a]prednK // mul2n -addnn addnS.
    have F4_c : 2 × c = 2 + c.-1 + c.-1.
      by rewrite -{1}[c]prednK // mul2n -addnn addnS.
    have F4 i k : 0 < i → S_[i.-1] k.+1 ≤ S_[(3 ×i).-2] k + i.-1.
      move⇒ i_gt0; apply: leq_trans (dsum_alpha3l _ _) _.
      rewrite leq_add2r.
      apply: (increasingE (increasing_dsum_alphaL_l _)).
      by rewrite -{2}[i]prednK // mulnS addSn add2n /=.
    have F4an := F4 a n a_gt0.
    have F4an1 := F4 a n.+1 a_gt0.
    have F4cn := F4 c n (c_gt0).
    have F4cn1 := F4 c n.+1 (c_gt0).
    have l_gt1 : 1 < l.
      by rewrite -ltnS l1E -[3]/(2 + 0 + 1); rewrite !leq_add.
    have F5 := SH l_gt1.
    have F6 : S_[l.+1] n.+2 + S_[1] n.+2 ≤ S_[a.-1] n.+2 + S_[(b + c).+2] n.+2.
      rewrite [X in _ ≤ X]addnC.
      rewrite (_ : l.+1 = 1 + a.-2 + (b + c).+1); last first.
        rewrite /b /c add1n -addSnnS !prednK //; last by rewrite -ltnS prednK.
        by rewrite addnCA addnA subnK // addnC subnK // ltnW.
      rewrite (_ : a.-1 = 1 + a.-2); last first.
         by rewrite add1n prednK // -ltnS prednK.
      by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).
    have F7 : S_[l] n.+1 + S_[1] n.+1 ≤ S_[a.-1] n.+1 + S_[(b + c).+1] n.+1.
      rewrite [X in _ ≤ X]addnC.
      rewrite (_ : l = 1 + a.-2 + (b + c)); last first.
        rewrite /b /c subSn // addnS -addSnnS add1n.
        rewrite !prednK //; last by rewrite -ltnS prednK.
        by rewrite addnCA addnA subnK // addnC subnK // ltnW.
      rewrite (_ : a.-1 = 1 + a.-2); last first.
         by rewrite add1n prednK // -ltnS prednK.
      by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).
    have F8 : S_[(b + c).+2] n.+2 + S_[1] n.+2 ≤ S_[c.-1] n.+2 + S_[b.+4] n.+2.
      rewrite (_ : (b + c).+2 = 1 + b.+3 + (c.-2)); last first.
        by rewrite add1n 2!addSnnS !prednK // -subn1 ltn_subRL addn0.
      rewrite (_ : c.-1 = 1 + c.-2); last first.
        by rewrite add1n prednK // -ltnS prednK.
      by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).
    have F9 : S_[(b + c).+1] n.+1 + S_[1] n.+1 ≤ S_[c.-1] n.+1 + S_[b.+3] n.+1.
      rewrite (_ : (b + c).+1 = 1 + b.+2 + (c.-2)); last first.
        by rewrite add1n 2!addSnnS !prednK // -subn1 ltn_subRL addn0.
      rewrite (_ : c.-1 = 1 + c.-2); last first.
        by rewrite add1n prednK // -ltnS prednK.
      by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).
    have F10 : S_[b.+4] n.+2 ≤ S_[b.+3] n.+1 + (α_[1] n.+1).*2.
      by apply: dsum_alphaL_alpha.
    have F11 : S_[b.+3] n.+1 ≤ S_[b.+2] n + (α_[1] n).*2.
      by apply: dsum_alphaL_alpha.
    have F12 : S_[b.+2] n + S_[1] n ≤ S_[b] n + S_[3] n.
      rewrite (_ : b.+2 = 1 + 2 + b.-1); last first.
        by rewrite add1n addSnnS prednK // ltnW.
      rewrite -{2}[b]prednK; last by apply: ltnW.
      by apply: concaveEk1 (concave_dsum_alphaL_l n).
    have F13 : S_[1] n.+1 = (S_[3] n).+1 by rewrite dsum_alpha3_S.
    have F14 := leq_dsum_alpha_2l_1 n.+1.
    have F15n := dsum_alphaL_S 1 n.+1.
    have F15n1 := dsum_alphaL_S 1 n.
    move: P3 P4 P5 P6 P7 P8 ⇒ P3 P4 P5 P6 P7 P8.
    applyr P3.
    rewrite -(leq_add2r x2S); applyr P4.
    rewrite -(leq_add2r y2S); applyr P5.
    rewrite -(leq_add2r (x3S + y3S)); applyr P6.
    rewrite -(leq_add2r (x4S + y4S)); applyr P7.
    rewrite -(leq_add2r (x5S + y5S)); applyr P8.
    applyl y4Sx5SE; applyl y3Sx4SE; applyl y2Sy5SE; applyl x2Sx3SE.
    gsimpl.
    rewrite ![2 × S_[_.-2] _]mul2n -!addnn {1}F1 {1}F2.
    rewrite {F1 F2}F3; gsimpl.
    rewrite {}F4_a {}F4_c.
    applyr F4an; applyr F4an1; applyr F4cn; applyr F4cn1.
    applyl F5.
    rewrite -(leq_add2r (S_[1] n.+2)); applyl F6.
    rewrite -(leq_add2r (S_[1] n.+1)); applyl F7.
    rewrite -(leq_add2r (S_[1] n.+2)); applyl F8.
    rewrite -(leq_add2r (S_[1] n.+1)); applyl F9; gsimpl.
    applyl F10.
    changel ((4 × S_[1] n + (α_[1] n.+1).*2 + S_[b.+3] n.+1).*2).
    changer ((2 + S_[2] n.+1 + S_[b] n + S_[2] n.+1 + S_[1] n.+2 +
      (S_[1] n.+1)).*2).
    rewrite leq_double.
    applyl F11; applyl F12; gsimpl; applyr F14.
    rewrite -ltnS -!addnS -F13.
    by rewrite {}F15n {}F15n1; gsimpl.
  move: b_le2; rewrite leq_eqVlt ⇒ /orP[/eqP[] bE1|].
    have a1E : a1 = a.+1 by rewrite -(subnK aLa1) -/b bE1.
    pose u3 := [ffun i : 'I_4 ⇒
                 if i == 0 :> nat then sam1
                 else if i == 1 :> nat then tam1
                 else if i == 2 :> nat then ↓[u (inord a)]
                 else ↓[u (inord a.+1)]].
    have cH6 (k : 'I_4) :
      0 < k < 3 → codom (u3 k) \subset [:: pa1S; a[p2, pa1] k].
      move⇒ /andP[k_gt0 k_lt3].
      rewrite !ffunE eqn_leq leqNgt k_gt0 /=.
      case: eqP ⇒ [->/=|/eqP kD1].
        by rewrite /pa1S !apegS apeg0 codom_apeg codom_subC.
      have ->/= : k = 2 :> nat.
        by apply/eqP; rewrite eqn_leq -ltnS k_lt3 ltn_neqAle eq_sym k_gt0 kD1.
      apply: codom_liftr; rewrite codom_subC.
      have /cH : 0 < (inord a : 'I_l.+2) < l.+1.
        rewrite inordK //.
        by rewrite a_gt0 /= l1E bE1 addn1 leq_addr.
      by rewrite inordK // /pa1S a1E !apegS apeg0.
    have P6 :
      (S_[3] n.+1).*2 ≤
      (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove +
          `d[↓[u (inord a)], ↓[u (inord a.+1)]]_smove) +
      sp sam1 3 p2 + sp ↓[u (inord a.+1)] 3 (a[p1, p3] a1).
      apply: (leq_trans (IH _ _ _ _ _ _ cH6)); rewrite /pa1S /pa1 //.
      - by rewrite eq_sym.
      - by rewrite eq_sym.
      - by rewrite apegS apeg_eqC eq_sym.
      repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.
      - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /=.
      - by apply: eq_bigr ⇒ i _; rewrite !ffunE /=.
      by apply: eq_bigr ⇒ i _; rewrite !ffunE.
    set x3S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6.
    have x2Sx3SE : x2S + x3S ≤ (S_[1] n).*2 + α_[maxn (3 × a).-2 3] n.
      by apply: sum_alpha_diffE; rewrite /pa.
    rewrite (maxn_idPl _) in x2Sx3SE; last first.
      by rewrite -subn2 ltn_subRL ltnW // (leq_mul2l 3 2).
    pose u5 := [ffun i : 'I_3 ⇒
                     if i == 0 :> nat then ↓[u (inord a1)]
                 else if i == 1 :> nat then sa1 else ta1].
    have cH8 (k : 'I_3) :
      0 < k < 2 → codom (u5 k) \subset [:: p1; a[p2, p3] k].
      move⇒ /andP[k_gt0 k_lt2].
      rewrite !ffunE.
      by have ->/= : k = 1 :> nat by case: (k : nat) k_gt0 k_lt2 ⇒ // [] [|].
    have P8 :
      (S_[2] n.+1).*2 ≤
      (`d[↓[u (inord a.+1)], sa1]_smove + `d[sa1, ta1]_smove) +
      sp ↓[u (inord a.+1)] 2 p2 + sp ta1 2 p2.
      apply: (leq_trans (IH _ _ _ _ _ _ cH8)) ⇒ //.
        by rewrite eq_sym.
      repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.
      - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK //= a1E.
      - by apply: eq_bigr ⇒ i _; rewrite !ffunE a1E.
      by apply: eq_bigr ⇒ i _; rewrite !ffunE.
    set x5S := sp _ _ _ in P8; set y5S := sp _ _ _ in P8.
    have y3Sx5SE : y3S + x5S ≤ (S_[1] n).*2 + α_[3] n.
      apply: sum_alpha_diffE ⇒ //.
      apply: codom_liftr; rewrite codom_subC.
      have := @cH (inord a.+1); rewrite inordK ?a1E //.
        by apply; rewrite andTb //= ltnS -a1E.
      by rewrite -a1E ltnS ltnW.
    have y5Sy2SE : y5S + y2S ≤ (S_[1] n).*2 + α_[maxn 2 (3 × c).-2] n.
      by apply: sum_alpha_diffE; rewrite // /pa1 eq_sym.
    rewrite (maxn_idPr _) in y5Sy2SE; last first.
      by rewrite -subn2 ltn_subRL (ltn_mul2l 3 1).
    rewrite (_ : sd u =
       \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove +
       \sum_(a ≤ i < a1) `d[u (inord i), u (inord i.+1)]_smove +
       \sum_(a1 ≤ i < l.+1) `d[u (inord i), u (inord i.+1)]_smove);
        last first.
      pose f i := `d[u (inord i), u (inord i.+1)]_smove.
      rewrite /sd -!(big_mkord xpredT f).
      by rewrite -!big_cat_nat //= ltnW.
    rewrite -{}P1 -{}P2; applyr P3.
    rewrite (_ : sd u1 =
              \sum_(i < (3 × a).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove
              + `d[sam1, tam1]_smove +
              `d[tam1, ↓[u (inord a)]]_smove); last first.
      pose f i := `d[u1 (inord i), u1 (inord i.+1)]_smove.
      rewrite /sd -!(big_mkord xpredT f) .
      rewrite -{1}(subnK (_ : 1 < 3 × a)) //; last first.
        by rewrite -[a]prednK // mulnS.
      rewrite subn2 !addn2 !big_nat_recr /f //=; congr (_ + _ + _).
        rewrite ffunE (_ : (3 × a).-2 = (3 × (a.-1)).+1); last first.
          by rewrite -{1}[a]prednK // mulnS.
        rewrite inordK; last by rewrite ltnS ltn_mul2l /= prednK.
        rewrite mod3E /= eqxx.
        rewrite ffunE inordK; last first.
          by rewrite -[_.+3](mulnDr 3 1) add1n prednK // ltnW.
        by rewrite mod3E /= eqxx.
      rewrite ffunE (_ : (3 × a).-2 = (3 × (a.-1)).+1); last first.
        by rewrite -{1}[a]prednK // mulnS.
      rewrite inordK; last first.
        by rewrite -{2}[a]prednK // mulnS.
      rewrite mod3E /= eqxx.
      rewrite ffunE inordK; last first.
        by rewrite -{2}[a]prednK // mulnS.
      by rewrite -[(_ × _).+3](mulnDr 3 1) mod3E /= div3E add1n prednK.
    rewrite (_ : sd u2 =
       `d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove +
               \sum_(i < (3 × c).-2)
                  `d[u2 (inord i.+2), u2 (inord i.+3)]_smove); last first.
      pose f i := `d[u2 (inord i), u2 (inord i.+1)]_smove.
      rewrite /sd -!(big_mkord xpredT f) .
      rewrite -{1}(subnK (_ : 1 < 3 × c)) //; last first.
        by rewrite -[c]prednK // mulnS.
      rewrite subn2 !addn2 !big_nat_recl // /f /= !addnA.
       congr (_ + _ + _).
      - rewrite !ffunE !inordK ?addn0 //=.
        by rewrite ltnS muln_gt0.
      - rewrite !ffunE !inordK //=.
          by rewrite ltnW // ltnS (leq_mul2l 3 1 c).
        by rewrite ltnS muln_gt0.
      by rewrite big_mkord.
    rewrite (_ : \sum_(_ ≤ _ < _) _ =
      `d[↓[u (inord a)], ↓[u (inord a.+1)]]_smove); last first.
      by rewrite a1E big_nat1.
    set z1S := \sum_(_ < _) _ in P4; set z2S := \sum_(_ < _) _ in P5.
    rewrite -/z1S -/z2S.
    rewrite -a1E in P8; set d2 := `d[_,_]_ _ + `d[_,_]_ _ in P8; rewrite -/d2.
    set d1 := `d[_,_]_ _ + `d[_,_]_ _ + `d[_,_]_ _ in P6.
    rewrite -/y1S.
    changer (2 × a + 2 × c + x1S + y1S + z1S + z2S + d2 +
              (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove +
               `d[↓[u (inord a)], ↓[u (inord a.+1)]]_smove)).
    rewrite -/d1.
    have F1 := dsum_alphaL_S (3 × a).-2 n.
    have F2 := dsum_alphaL_S (3 × c).-2 n.
    have F3 := dsum_alphaL_S 3 n.
    have F4_a : 2 × a = 2 + a.-1 + a.-1.
      by rewrite -{1}[a]prednK // mul2n -addnn addnS.
    have F4_c : 2 × c = 2 + c.-1 + c.-1.
      by rewrite -{1}[c]prednK // mul2n -addnn addnS.
    have F4 i k : 0 < i → S_[i.-1] k.+1 ≤ S_[(3 ×i).-2] k + i.-1.
      move⇒ i_gt0; apply: leq_trans (dsum_alpha3l _ _) _.
      rewrite leq_add2r.
      apply: (increasingE (increasing_dsum_alphaL_l _)).
      by rewrite -{2}[i]prednK // mulnS addSn add2n /=.
    have F4an := F4 a n a_gt0.
    have F4an1 := F4 a n.+1 a_gt0.
    have F4cn := F4 c n (c_gt0).
    have F4cn1 := F4 c n.+1 (c_gt0).
    have l_gt1 : 1 < l.
      by rewrite -ltnS l1E -[3]/(2 + 0 + 1); rewrite !leq_add.
    have F5 := SH l_gt1.
    have F6n : S_[1] n.+1 = (S_[3] n).+1 by rewrite dsum_alpha3_S.
    have F6n1 : S_[1] n.+2 = (S_[3] n.+1).+1 by rewrite dsum_alpha3_S.
    have am1_gt0 : 0 < a.-1 by rewrite -subn1 ltn_subRL addn0.
    have F7n1 : S_[1] n.+2 + S_[l.+1] n.+2 ≤ S_[a.-1] n.+2 + S_[c.+3] n.+2.
      rewrite addnC (_ : l.+1 = 1 + c.+2 + a.-2); last first.
        by rewrite /c a1E add1n !addSnnS !prednK ?subnK // -a1E ltnW.
      rewrite {2}(_ : a.-1 = 1 + a.-2); last by rewrite add1n prednK.
      by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).
    have F7n : S_[1] n.+1 + S_[l] n.+1 ≤ S_[a.-1] n.+1 + S_[c.+2] n.+1.
      rewrite addnC (_ : l = 1 + c.+1 + a.-2); last first.
        by rewrite /c a1E add1n subSS !addSnnS !prednK ?subnK // -ltnS -a1E ltnW.
      rewrite {2}(_ : a.-1 = 1 + a.-2); last by rewrite add1n prednK.
      by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).
    have cm1_gt0 : 0 < c.-1 by rewrite -subn1 ltn_subRL addn0.
    have F8n1 : S_[1] n.+2 + S_[c.+3] n.+2 ≤ S_[c.-1] n.+2 + S_[5] n.+2.
      rewrite addnC (_ : c.+3 = 1 + 4 + c.-2); last first.
        by rewrite add1n 2!addSnnS !prednK.
      rewrite {2}(_ : c.-1 = 1 + c.-2); last by rewrite add1n prednK.
      by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).
    have F8n : S_[1] n.+1 + S_[c.+2] n.+1 ≤ S_[c.-1] n.+1 + S_[4] n.+1.
      rewrite addnC (_ : c.+2 = 1 + 3 + c.-2); last first.
        by rewrite add1n 2!addSnnS !prednK.
      rewrite {2}(_ : c.-1 = 1 + c.-2); last by rewrite add1n prednK.
      by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).
    have F9 : S_[5] n.+2 ≤ S_[4] n.+1 + (α_[1] n.+1).*2.
      by apply: dsum_alphaL_alpha.
    have F10 : S_[4] n.+1 ≤ S_[3] n + (α_[1] n).*2.
      by apply: dsum_alphaL_alpha.
    have F11 : S_[1] n.+1 = (S_[3] n).+1 by rewrite dsum_alpha3_S.
    have F12 := leq_dsum_alpha_2l_1 n.+1.
    have F13n1 := dsum_alphaL_S 1 n.+1.
    have F13n := dsum_alphaL_S 1 n.
    move: P4 P5 P6 P8 ⇒ P4 P5 P6 P8.
    rewrite -(leq_add2r x2S); applyr P4.
    rewrite -(leq_add2r y2S); applyr P5.
    rewrite -(leq_add2r (x3S + y3S)); applyr P6.
    rewrite -(leq_add2r (x5S + y5S)); applyr P8.
    applyl y5Sy2SE; applyl y3Sx5SE; applyl x2Sx3SE.
    rewrite [2 × (S_[_.-2] _)]mul2n -addnn {1}F1.
    rewrite [2 × (S_[_.-2] _)]mul2n -addnn {1}F2.
    rewrite [2 × (S_[3] _)]mul2n -addnn {1}F3.
    gsimpl.
    rewrite {}F4_a {}F4_c.
    applyr F4an; applyr F4an1; applyr F4cn; applyr F4cn1.
    applyl F5.
    rewrite -ltnS -!addSn -!addnA [X in _ ≤ X]addnC !addnA -ltnS -!addSn.
    rewrite -{}F6n -{}F6n1.
    rewrite -(leq_add2r (S_[1] n.+2)); applyl F7n1.
    rewrite -(leq_add2r (S_[1] n.+1)); applyl F7n; gsimpl.
    rewrite -(leq_add2r (S_[1] n.+2)); applyl F8n1.
    rewrite -(leq_add2r (S_[1] n.+1)); applyl F8n; gsimpl.
    applyl F9.
    rewrite -leq_double in F10; applyl F10.
    rewrite -(leq_add2r 2).
    changel (6 × S_[1] n + 4 × α_[1] n.+1 + (α_[1] n).*2 + (α_[1] n).*2 +
      ((S_[3] n).+1).*2).
    rewrite -{}F11.
    applyr F12.
    by rewrite F13n1 F13n; gsimpl.
  rewrite !ltnS leqn0 ⇒ /eqP bE0.
  have a1E : a1 = a by rewrite -(subnK aLa1) -/b bE0.
  pose u3 := [ffun i : 'I_5 ⇒
                 if i == 0 :> nat then sam1
                 else if i == 1 :> nat then tam1
                 else if i == 2 :> nat then ↓[u (inord a)]
                 else if i == 3 :> nat then sa1
                 else ta1].
  have cH6 (k : 'I_5) :
    0 < k < 4 → codom (u3 k) \subset [:: pa1; a[p2, pa1S] k].
    move⇒ /andP[k_gt0 k_lt3].
    rewrite !ffunE eqn_leq leqNgt k_gt0 /=.
    case: eqP ⇒ [->/=|/eqP kD1].
      by rewrite /pa1S !apegS apeg0 codom_apeg.
    case: eqP =>[->/=|/eqP kD2].
      apply: codom_liftr; rewrite codom_subC.
      have /cH : 0 < (inord a : 'I_l.+2) < l.+1.
        by rewrite inordK // a_gt0 /= -a1E.
      by rewrite inordK // /pa1 a1E.
    have ->/= : k = 3 :> nat.
      by case: (k : nat) k_lt3 k_gt0 kD1 kD2 ⇒ // [] [|[|[|]]].
    by rewrite /pa1S !(apegS, apeg0) codom_apeg.
  have P6 :
    (S_[4] n.+1).*2 ≤
    (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove +
        `d[↓[u (inord a)], sa1]_smove +
        `d[sa1, ta1]_smove) + sp sam1 4 p2 + sp ta1 4 p2.
    apply: (leq_trans (IH _ _ _ _ _ _ cH6)); rewrite /pa1S /pa1 //.
    - by rewrite eq_sym.
    - by rewrite eq_sym.
    - by rewrite apegS apeg_eqC.
    repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.
    - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /= ?a1E.
    - by apply: eq_bigr ⇒ i _; rewrite !ffunE /=.
    by apply: eq_bigr ⇒ i _; rewrite !ffunE /= a1E.
  set x3S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6.
  have x2Sx3SE : x2S + x3S ≤ (S_[1] n).*2 + α_[maxn (3 × a).-2 4] n.
    by apply: sum_alpha_diffE; rewrite /pa.
  rewrite (maxn_idPl _) in x2Sx3SE; last first.
    by rewrite -subn2 ltn_subRL // (leq_mul2l 3 2).
  have y2Sy3SE : y2S + y3S ≤ (S_[1] n).*2 + α_[maxn (3 × c).-2 4] n.
    apply: sum_alpha_diffE ⇒ //; first by rewrite /pa1.
    by rewrite codom_subC.
  rewrite (maxn_idPl _) in y2Sy3SE; last first.
    by rewrite -subn2 ltn_subRL (leq_mul2l 3 2).
  rewrite (_ : sd u =
      \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove +
      \sum_(a1 ≤ i < l.+1) `d[u (inord i), u (inord i.+1)]_smove); last first.
    pose f i := `d[u (inord i), u (inord i.+1)]_smove.
    by rewrite /sd -!(big_mkord xpredT f) a1E -!big_cat_nat.
  rewrite -{}P1 -{P3}P2.
  rewrite (_ : sd u1 =
            \sum_(i < (3 × a).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove
            + `d[sam1, tam1]_smove
            + `d[tam1, ↓[u (inord a)]]_smove); last first.
    pose f i := `d[u1 (inord i), u1 (inord i.+1)]_smove.
    rewrite /sd -!(big_mkord xpredT f) .
    rewrite -{1}(subnK (_ : 1 < 3 × a)) //; last first.
      by rewrite -[a]prednK // mulnS.
    rewrite subn2 !addn2 !big_nat_recr /f //=; congr (_ + _ + _).
      rewrite ffunE (_ : (3 × a).-2 = (3 × (a.-1)).+1); last first.
        by rewrite -{1}[a]prednK // mulnS.
      rewrite inordK; last by rewrite ltnS ltn_mul2l /= prednK.
      rewrite mod3E /= eqxx.
      rewrite ffunE inordK; last first.
        by rewrite -[_.+3](mulnDr 3 1) add1n prednK // ltnW.
      by rewrite mod3E /= eqxx.
    rewrite ffunE (_ : (3 × a).-2 = (3 × (a.-1)).+1); last first.
      by rewrite -{1}[a]prednK // mulnS.
    rewrite inordK; last first.
      by rewrite -{2}[a]prednK // mulnS.
    rewrite mod3E /= eqxx.
    rewrite ffunE inordK; last first.
      by rewrite -{2}[a]prednK // mulnS.
    by rewrite -[(_ × _).+3](mulnDr 3 1) mod3E /= div3E add1n prednK.
  rewrite [X in _ ≤ _ + (_ + X) + _ + _](_ : _ =
      `d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove +
      \sum_(i < (3 × c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove);
       last first.
    pose f i := `d[u2 (inord i), u2 (inord i.+1)]_smove.
    rewrite /sd -!(big_mkord xpredT f) .
    rewrite -{1}(subnK (_ : 1 < 3 × c)) //; last first.
      by rewrite -[c]prednK // mulnS.
    rewrite subn2 !addn2 !big_nat_recl // /f /= !addnA; congr (_ + _ + _).
    - rewrite !ffunE !inordK ?addn0 //=.
      by rewrite ltnS muln_gt0.
    - rewrite !ffunE !inordK //=.
        by rewrite ltnW // ltnS (leq_mul2l 3 1 c).
      by rewrite ltnS muln_gt0.
    by rewrite big_mkord.
  set z1S := \sum_(_ < _) _ in P4; set z2S := \sum_(_ < _) _ in P5.
  rewrite -/z1S -/z2S.
  rewrite a1E -/y1S.
  changer (a.*2 + c.*2 + (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove
    + `d[↓[u (inord a)], sa1]_smove + `d[sa1, ta1]_smove)
    + x1S + y1S + z1S + z2S).
  set d1 := `d[_,_]_ _ + `d[_,_]_ _ + `d[_,_]_ _ + `d[_,_]_ _;
    rewrite -/d1 in P6.
  have F1 := dsum_alphaL_S (3 × a).-2 n.
  have F2 := dsum_alphaL_S (3 × c).-2 n.
  have F3 := dsum_alphaL_S 4 n.
  have F4_a : 2 × a = 2 + a.-1 + a.-1.
    by rewrite mul2n -{1}[a]prednK // -addnn addnS.
  have F4_c : 2 × c = 2 + c.-1 + c.-1.
    by rewrite mul2n -{1}[c]prednK // -addnn addnS.
  have F4 i k : 0 < i → S_[i.-1] k.+1 ≤ S_[(3 ×i).-2] k + i.-1.
    move⇒ i_gt0; apply: leq_trans (dsum_alpha3l _ _) _.
    rewrite leq_add2r.
    apply: (increasingE (increasing_dsum_alphaL_l _)).
    by rewrite -{2}[i]prednK // mulnS addSn add2n /=.
  have F4an := F4 a n a_gt0.
  have F4an1 := F4 a n.+1 a_gt0.
  have F4cn := F4 c n (c_gt0).
  have F4cn1 := F4 c n.+1 (c_gt0).
  have l_gt1 : 1 < l.
    by rewrite -ltnS l1E -[3]/(2 + 0 + 1); rewrite !leq_add.
  have F5 := SH l_gt1.
  have am1_gt0 : 0 < a.-1 by rewrite -subn1 ltn_subRL addn0.
  have F6n1 : S_[1] n.+2 + S_[l.+1] n.+2 ≤ S_[a.-1] n.+2 + S_[c.+2] n.+2.
    rewrite addnC (_ : l.+1 = 1 + c.+1 + a.-2); last first.
      by rewrite /c add1n 2!addSnnS !prednK ?a1E ?subnK.
    rewrite {2}(_ : a.-1 = 1 + a.-2); last by rewrite add1n prednK.
    by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).
  have F6n : S_[1] n.+1 + S_[l] n.+1 ≤ S_[a.-1] n.+1 + S_[c.+1] n.+1.
    rewrite addnC (_ : l = 1 + c + a.-2); last first.
      rewrite /c add1n a1E -{1}[a]prednK // subSS.
      by rewrite !addSnnS !prednK // subnK // -ltnS prednK.
    rewrite {2}(_ : a.-1 = 1 + a.-2); last by rewrite add1n prednK.
    by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).
  have cm1_gt0 : 0 < c.-1 by rewrite -subn1 ltn_subRL addn0.
  have F7n1 : S_[1] n.+2 + S_[c.+2] n.+2 ≤ S_[c.-1] n.+2 + S_[4] n.+2.
    rewrite addnC (_ : c.+2 = 1 + 3 + c.-2); last first.
      by rewrite add1n 2!addSnnS !prednK.
    rewrite {2}(_ : c.-1 = 1 + c.-2); last by rewrite add1n prednK.
    by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).
  have F7n : S_[1] n.+1 + S_[c.+1] n.+1 ≤ S_[c.-1] n.+1 + S_[3] n.+1.
    rewrite addnC (_ : c.+1 = 1 + 2 + c.-2); last first.
      by rewrite add1n 2!addSnnS !prednK.
    rewrite {2}(_ : c.-1 = 1 + c.-2); last by rewrite add1n prednK.
    by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).
  have F8 : S_[4] n.+2 ≤ S_[3] n.+1 + (α_[1] n.+1).*2.
    by apply: dsum_alphaL_alpha n.+1 (isT : 1 < 3).
  have F9 : S_[3] n.+1 ≤ S_[4] n.+1 by case: (concave_dsum_alphaL_l n.+1).
  have F10n1 := dsum_alphaL_S 1 n.+1.
  have F10n := dsum_alphaL_S 1 n.
  have F11 := bound_alphaL 2 n.
  have F12 := alphaL_1_2 n.
  move: P4 P5 P6 ⇒ P4 P5 P6.
  rewrite -(leq_add2r x2S); applyr P4.
  rewrite -(leq_add2r y2S); applyr P5.
  rewrite -(leq_add2r (x3S + y3S)); applyr P6.
  applyl x2Sx3SE; applyl y2Sy3SE; gsimpl.
  rewrite [2 × (S_[_.-2] _)]mul2n -addnn {1}F1.
  rewrite [2 × (S_[_.-2] _)]mul2n -addnn {1}F2.
  gsimpl.
  rewrite {}F4_a {}F4_c.
  applyr F4an1; applyr F4an; applyr F4cn1; applyr F4cn.
  applyl F5.
  rewrite -(leq_add2r (S_[c.+2] n.+2)); applyr F6n1.
  rewrite -(leq_add2r (S_[c.+1] n.+1)); applyr F6n; gsimpl.
  rewrite -(leq_add2r (S_[1] n.+2)); applyl F7n1.
  rewrite -(leq_add2r (S_[1] n.+1)); applyl F7n.
  applyl F8; gsimpl.
  changel ((α_[1] n.+1).*2 + (S_[1] n).*2 + (S_[1] n).*2 +
    (α_[1] n.+1).*2 + (S_[3] n.+1).*2).
  changer (4 + S_[1] n.+2 + S_[1] n.+1 + S_[1] n.+2 + S_[1] n.+1 +
    (S_[4] n.+1).*2).
  apply: leq_add; last by rewrite leq_double.
  rewrite F10n1 F10n; gsimpl.
  by rewrite -leq_double in F12; applyl F12; gsimpl.
rewrite negb_and -!leqNgt ⇒ acH.
have aLc : a ≤ c by [].
have aE1 : a = 1.
  case/orP: acH; case: (a) aLc a_gt0 ⇒ // [] [|n1] //.
  by case: (c) ⇒ // [] [].
have leq_S4 k : 5 × S_[1] k.+1 + S_[1] k.+2 ≤ 6 × S_[4] k + 9.
  have F3 : 4 × S_[3] k + 2 × S_[6] k ≤ 6 × S_[4] k.
    rewrite -{1}[4]/(2 × 2) -mulnA -mulnDr -{2}[6]/(2 × 3) -mulnA.
    rewrite leq_mul2l /= -(leq_add2r (S_[5] k)).
    changel (S_[6] k + S_[3] k + (S_[5] k + S_[3] k)).
    changer (S_[5] k + S_[4] k + (S_[4] k + S_[4] k)).
    by apply: leq_add; apply: concaveEk1 3 _ _ (concave_dsum_alphaL_l k).
  applyr F3.
  have F3k : S_[1] k.+1 ≤ S_[3] k + 1 by apply: dsum_alpha3l.
  have F3k1 : S_[2] k.+1 ≤ S_[6] k + 2 by apply: dsum_alpha3l.
  rewrite -leq_double in F3k1; applyr F3k1.
  rewrite -2!leq_double in F3k; applyr F3k; gsimpl.
  by have F4 := leq_dsum_alpha_2l_1 k.+1; applyr F4.
move: c_gt0; rewrite leq_eqVlt eq_sym ⇒ /orP[/eqP cE1|c_gt1].
  move : P1 P2 P3 ⇒ P1 P2 P3.
  have l_gt0 : 0 < l by rewrite -ltnS l1E aE1 cE1 addn1.
  have a1El : a1 = l.
    by rewrite -(subKn (_ : a1 ≤ l.+1)) 1?ltnW // -/c cE1 subSS subn0.
  have [b_gt1|b_lt2]:= leqP 2 b.
    rewrite (_ : sd u =
        \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove +
        \sum_(a ≤ i < a1) `d[u (inord i), u (inord i.+1)]_smove +
        \sum_(a1 ≤ i < l.+1) `d[u (inord i), u (inord i.+1)]_smove);
        last first.
      pose f i := `d[u (inord i), u (inord i.+1)]_smove.
      rewrite /sd -!(big_mkord xpredT f).
      by rewrite -!big_cat_nat //= ltnW.
    rewrite !sum_beta_S // KH1 eqxx addn0 KH2 eqxx addn0.
    apply: leq_trans (leq_add (leq_add (leq_add (leq_add (leqnn _) P3)
                       (leqnn _)) (leqnn _)) (leqnn _)); rewrite -{P3}P1 -{}P2.
    set x2S := sd u2; set x0S := sd u1.
    pose u3 := [ffun i : 'I_b.+1 ⇒ ↓[u (inord (a + i))]].
    rewrite (_ : \sum_(_ ≤ _ < _) _ =
        \sum_(i < b) `d[u3 (inord i), u3 (inord i.+1)]_smove); last first.
      rewrite -{1}[a]add0n big_addn -/b big_mkord.
      apply: eq_bigr ⇒ i _.
      by rewrite !ffunE addnC !inordK ?(addnS, ltnS) // ltnW.
    pose paS := a[p1, p3] a.+1.
    have cH3 (k : 'I_b.+1) :
      0 < k < b → codom (u3 k) \subset [:: p2; a[pa, paS] k].
      move⇒ /andP[k_gt0 k_ltb].
      have akLl : a + k < l.+1.
        rewrite ltnS (leq_trans _ a1Ll) //.
        by rewrite -(subnK aLa1) addnC leq_add2r ltnW.
      rewrite !ffunE.
      have /H : 0 < (inord (a + k) : 'I_l.+2) < l.+1.
        rewrite inordK; first by rewrite addn_gt0 a_gt0.
        by rewrite ltnS ltnW.
      rewrite ffunE inordK //; last by rewrite ltnS ltnW.
      by rewrite /paS apegS -apegD [k + _]addnC.
    pose pa1 := a[p1, p3] a1.
    have P3 :
      (S_[b] n.+1).*2 ≤
      \sum_(i < b) `d[↓[u (inord (a + i))], ↓[u (inord (a + i).+1)]]_smove +
      sp ↓[u (inord a)] b pa + sp ↓[u (inord a1)] b pa1.
      apply: leq_trans (IH _ _ _ _ _ _ cH3) (leq_add (leq_add _ _) _);
        rewrite /pa /paS // 1?eq_sym //.
      - by rewrite apegS apeg_eqC eq_sym.
      - apply: leq_sum ⇒ i; rewrite !ffunE !inordK ?addnS //.
          by rewrite ltnS.
        by rewrite ltnS ltnW.
      - by apply: leq_sum ⇒ i _; rewrite !ffunE addn0.
      apply: leq_sum ⇒ i _; rewrite !ffunE /= [a + b]addnC subnK //.
      by rewrite apegS -apegD subnK.
    set x1S := \sum_(_ < _) _ in P3; set y2S := sp _ _ _ in P3.
    set y3S := sp _ _ _ in P3.
    rewrite [\sum_(_ < _) _](_ : _ = x1S); last first.
      by apply: eq_bigr ⇒ i; rewrite !ffunE !inordK ?addnS // ltnS // ltnW.
    set y0S := \sum_(_ < _) _ ; set y5S := \sum_(_ < _) _.
    have cH1 (k : 'I_(3 × a).+1) :
      0 < k < 3 × a → codom (u1 k) \subset [:: p3; a[p1, p2] k].
      move⇒ /andP[k_gt0 k_ltb].
      rewrite {2}aE1 muln1 in k_ltb.
      rewrite ffunE !modn_small // !divn_small // inord_eq0 //.
      rewrite [in 3 × a.-1]aE1 /=.
      case: (k : nat) k_gt0 k_ltb ⇒ //= [] [|[|]] //= _ _.
        rewrite !(apegS, apeg0).
        by have := sam1C; rewrite /pa aE1 apegS apeg0.
      by rewrite !(apegS, apeg0) codom_subC.
    have P1 :
      (S_[3 × a] n.+1).*2 ≤ x0S + sp ↓[u ord0] 3 p1 + sp ↓[u (inord a)] 3 p2.
      apply: leq_trans (IH _ _ _ _ _ _ cH1) (leq_add (leq_add _ _) _);
          rewrite // 1?eq_sym //.
        by apply: leq_sum ⇒ i _; rewrite ffunE /= inord_eq0 // aE1 muln1.
      by apply: leq_sum ⇒ i _; rewrite ffunE /= mod3E /= div3E // aE1 muln1.
    have {}P1 := leq_trans P1 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                          (leqnn _)).
    rewrite -/y0S in P1; set y1S := sp _ _ _ in P1.
    rewrite aE1 muln1 in P1.
    have y1Sy2SE : y1S + y2S ≤ (S_[1] n).*2 + α_[maxn 3 b] n.
      apply: sum_alpha_diffE ⇒ //; first by rewrite /pa // eq_sym.
      apply: codom_liftr.
      have /cH : 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK.
      by rewrite /pa aE1 inordK.
    have cH2 (k : 'I_(3 × c).+1) :
      0 < k < 3 × c →
      codom (u2 k) \subset [:: a[p1, p3] a1; a[p2, a[p1, p3] a1.+1] k].
      move⇒ /andP[k_gt0 k_ltb].
      rewrite {2}cE1 muln1 in k_ltb.
      rewrite ffunE !modn_small // !divn_small // addn0.
      case: (k : nat) k_gt0 k_ltb ⇒ //= [] [|[|]] //= _ _.
        by rewrite !apegS apeg0 codom_apeg.
      by rewrite !(apegS, apeg0) codom_subC.
    have P2 :
      (S_[3 × c] n.+1).*2 ≤ x2S + sp ↓[u (inord a1)] 3 p2 +
                             sp ↓[u ord_max] 3 (a[p3, p1] l).
      apply: leq_trans (IH _ _ _ _ _ _ cH2) (leq_add (leq_add _ _) _);
          rewrite // 1?eq_sym //.
      - by rewrite apegS apeg_eqC eq_sym.
      - by apply: leq_sum ⇒ i _; rewrite ffunE /= addn0 cE1 muln1.
      apply: leq_sum ⇒ i _; rewrite ffunE /= mod3E /= div3E // cE1 muln1.
      rewrite a1El addn1 (_ : inord _ = ord_max) ?apegS //.
      by apply/val_eqP; rewrite /= inordK.
    have {}P2 := leq_trans P2 (leq_add (leqnn _) (leq_sum_beta _ _)).
    rewrite -/y5S in P2; set y4S := sp _ _ _ in P2.
    have y3Sy4SE : y3S + y4S ≤ (S_[1] n).*2 + α_[maxn b 3] n.
      apply: sum_alpha_diffE; rewrite /pa /pa1 //.
      apply: codom_liftr; rewrite codom_subC.
      have /cH : 0 < (inord l : 'I_l.+2) < l.+1 by rewrite inordK // l_gt0 /=.
      by rewrite a1El inordK.
    have Eb1 : l = b.+1.
      by have := l1E; rewrite aE1 cE1 addn1 ⇒ [] [].
    rewrite Eb1.
    have F1b := dsum_alphaL_S b n.
    have F1n31 : (S_[3] n.+1).+1 = S_[1] n.+2.
      by rewrite dsum_alpha3_S.
    have F1n1 := dsum_alphaL_S 1 n.
    have F1n2 := dsum_alphaL_S 1 n.+1.
    have b_gt0 : 0 < b by apply: leq_trans b_gt1.
    have F2n1 : S_[b.+2] n.+2 ≤ S_[b.+1] n.+1 + (α_[1] n.+1).*2.
      by rewrite dsum_alphaL_alpha .
    have F2n : S_[b.+1] n.+1 ≤ S_[b] n + (α_[1] n).*2.
      by rewrite dsum_alphaL_alpha.
    have F3n : S_[4] n.+2 ≤ S_[3] n.+1 + (α_[1] n.+1).*2.
      by rewrite dsum_alphaL_alpha.
    have F4n := alphaL_3E n.
    have F5 := leq_dsum_alpha_2l_1 n.+1.
    move: P1 P2 P3 ⇒ P1 P2 P3.
    rewrite -(leq_add2r y1S); applyr P1.
    rewrite -(leq_add2r y4S); applyr P2.
    rewrite -(leq_add2r (y2S + y3S)); applyr P3.
    applyl y3Sy4SE; applyl y1Sy2SE; gsimpl.
    rewrite maxnC aE1 cE1 !muln1.
    changel ((S_[b.+2] n.+2 + (S_[1] n).*2 + α_[maxn 3 b] n).*2).
    changer (((S_[3] n.+1).+1.*2 + S_[b] n.+1).*2).
    rewrite leq_double.
    move: b_gt1; rewrite leq_eqVlt ⇒ /orP[/eqP<-|b_gt2]; last first.
      rewrite (maxn_idPr _) //.
      rewrite F1b addnA leq_add2r F1n31 F1n2 F1n1.
      by applyr F2n; applyr F2n1; gsimpl.
    rewrite (maxn_idPl _) //.
    applyl F3n; gsimpl.
    rewrite -ltnS -![in X in _ ≤ X]addSn !{}F1n31 {}F4n; gsimpl.
    rewrite F1n2; gsimpl.
    have [n_gt3 |] := leqP 4 n; last first.
      by case: n ⇒ [|[|[|[|n1]]]]; rewrite // !(alphaS_small, alpha_small).
    rewrite -leq_double; applyr F5.
    rewrite F1n2 F1n1; gsimpl.
    by have F := alpha_4_3 (n_gt3); applyr F.
  move: b_lt2; rewrite leq_eqVlt ⇒ /orP[/eqP [] bE1 | b_lt1].
    pose u1l :=
      [ffun i ⇒
        if (i : 'I_5) == 0 :> nat then ↓[u ord0] else
        if i == 1 :> nat then sam1 else
        if i == 2 :> nat then tam1 else
        if i == 3 :> nat then ↓[u (inord 1)] else ↓[u (inord 2)]].
    have a1E2 : a1 = 2.
      by move: (cE1); rewrite /c l1E aE1 bE1 cE1; case: (a1) ⇒ // [] [|[|]].
    have P1l1 : a.*2 + sd u1l ≤
      \sum_(i < a1) `d[u (inord i), u (inord i.+1)]_smove.
      rewrite /sd a1E2 !big_ord_recr /= !big_ord0 !add0n {1}aE1.
      rewrite !ffunE /= !inordK ?aE1 //= add2n -2!addSn leq_add //; last first.
        by apply/gdist_cunlift/shanoi_connect.
      rewrite (inord_eq0 _ (_ : 0 = 0)) //.
      rewrite (_ : ord0 = inord a.-1); last first.
        by apply/val_eqP; rewrite /= inordK aE1.
      by rewrite -[in inord 1]aE1 duam1ua1E /= addnA addn0.
    have cH1 (k : 'I_5) :
      0 < k < 4 → codom (u1l k) \subset [:: p3; a[p1, p2] k].
      case: k ⇒ [] [|[|[|[|]]]] //= iH _; rewrite !ffunE !(apegS, apeg0).
      - by have := sam1C; rewrite /pa aE1.
      - by rewrite codom_subC.
      apply: codom_liftr; rewrite codom_subC.
      have /cH: 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK.
      by rewrite inordK.
    have lE2 : l = 2 by move: l1E; rewrite aE1 bE1 cE1 ⇒ [] [].
    have {cH1}P4 :
      (S_[4] n.+1).*2 ≤ sd u1l + sp ↓[u ord0] 4 p1 +
                                  sp ↓[u (inord a1)] 4 p1.
      apply: leq_trans (IH _ _ _ _ _ _ cH1) _ ⇒ //.
        by rewrite eq_sym.
      repeat apply: leq_add ⇒ //; apply: leq_sum ⇒ i /= _; rewrite !ffunE //.
      by rewrite a1El -[in inord 2]lE2.
    have {}P4 := leq_trans P4 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                                    (leqnn _)).
    set x1S := sd _ in P4.
    set y1S := \sum_(_ < _) _ in P4; set y2S := sp _ _ _ in P4.
    have cH2 (k : 'I_(3 × c).+1) :
      0 < k < 3 × c →
      codom (u2 k) \subset [:: a[p1, p3] a1; a[p2, a[p1, p3] a1.+1] k].
      move⇒ /andP[k_gt0 k_ltb].
      rewrite {2}cE1 muln1 in k_ltb.
      rewrite ffunE !modn_small // !divn_small // addn0.
      case: (k : nat) k_gt0 k_ltb ⇒ //= [] [|[|]] //= _ _.
        by rewrite a1E2.
      by rewrite codom_subC.
    have P5 :
      (S_[3 × c] n.+1).*2 ≤ sd u2 + sp ↓[u (inord a1)] 3 p2 +
                                     sp ↓[u ord_max] 3 (a[p3, p1] l).
      apply: leq_trans (IH _ _ _ _ _ _ cH2) (leq_add (leq_add _ _) _);
          rewrite // 1?eq_sym //.
      - by rewrite a1E2 eq_sym.
      - by apply: leq_sum ⇒ i _; rewrite ffunE /= addn0 cE1 muln1.
      apply: leq_sum ⇒ i _; rewrite ffunE /= mod3E /= div3E // cE1 muln1.
      rewrite a1El addn1 (_ : inord _ = ord_max) ?apegS //.
      by apply/val_eqP; rewrite /= inordK.
    have {}P5 := leq_trans P5 (leq_add (leqnn _) (leq_sum_beta _ _)).
    rewrite // {1}[in 3 ×c]cE1 muln1 in P5.
    set x2S := sd _ in P5.
    set y3S := sp _ _ _ in P5; set y4S := \sum_(_ < _) _ in P5.
    rewrite /sd -(big_mkord xpredT
                   (fun i ⇒ `d[u (inord i), u (inord i.+1)]_smove)).
    rewrite (big_cat_nat _ _ _ (_ : 0 ≤ a1)) //=; last by apply: ltnW.
    rewrite big_mkord -!addnA.
    apply: leq_trans (leq_add P1l1 (leqnn _)); rewrite -/x1S.
    rewrite -{P1l1}P2 -/x2S {1}lE2 !sum_beta_S //.
    rewrite KH1 KH2 !eqxx !addn0 aE1 -/y1S -/y4S.
    have y2Sy3SE : y2S + y3S ≤ (S_[1] n).*2 + α_[4] n.
      apply: sum_alpha_diffE ⇒ //.
      apply: codom_liftr; rewrite codom_subC.
      have /cH : 0 < (inord a1 : 'I_l.+2) < l.+1 by rewrite inordK // a1E2 lE2.
      by rewrite inordK // a1E2.
    rewrite {1}aE1 -[1.*2]/2 in P1.
    rewrite {1}cE1 -[1.*2]/2.
    have F1n4 := dsum_alphaL_S 4 n.
    have F1n3 : (S_[3] n.+2).+1 = S_[1] n.+3.
      by rewrite -dsum_alpha3_S.
    have F1n13 : (S_[3] n.+1).+1 = S_[1] n.+2.
      by rewrite -dsum_alpha3_S.
    move: P4 P5 ⇒ P4 P5.
    rewrite -(leq_add2r y2S); applyr P4.
    rewrite -(leq_add2r y3S); applyr P5.
    applyl y2Sy3SE.
    rewrite [in X in _ ≤ X]mul2n -addnn.
    rewrite {1}F1n4; gsimpl.
    rewrite -(leq_add2r 2).
    changel (((S_[3] n.+2).+1).*2 + (S_[1] n).*2).
    changer (4 + S_[4] n + S_[4] n.+1 + ((S_[3] n.+1).+1).*2).
    rewrite {}F1n3 {}F1n13.
    case : n ⇒ [|[|[|[|n1]]]]; try by rewrite !alphaS_small.
    set m1 := n1.+3.
    rewrite -(leq_add2r (S_[1] m1.+2).*2).
    rewrite -[_ ≤ _](leq_mul2l 6).
    have F := leq_S4 m1.+1; applyr F.
    have F := leq_S4 m1.+2; applyr F; gsimpl.
    have F3n3 := dsum_alphaL_S 1 m1.+3.
    have F3n2 := dsum_alphaL_S 1 m1.+2.
    have F3n1 := dsum_alphaL_S 1 m1.+1.
    rewrite !(F3n3, F3n2, F3n1); gsimpl.
    have F4m1 : 12 × α_[1] m1.+3 ≤ 16 × α_[1] m1.+2.
      rewrite -[12]/(4 × 3) -mulnA.
      rewrite -[16]/(4 × 4) -mulnA leq_mul2l /=.
      by rewrite alpha_4_3.
    apply: leq_trans (leq_trans _ F4m1) _; first by rewrite leq_mul2r orbT.
    gsimpl.
    have F4m2 : 9 × α_[1] m1.+2 ≤ 12 × α_[1] m1.+1.
      rewrite -[12]/(3 × 4) -mulnA.
      rewrite -[9]/(3 × 3) -mulnA leq_mul2l /=.
      by rewrite alpha_4_3.
    by applyr F4m2; gsimpl.
  have bE0 : b = 0 by case: (b) b_lt1 ⇒ //.
  have lE1 : l = 1 by have := l1E; rewrite aE1 bE0 cE1 ⇒ [] [].
  have a1E1 : a1 = 1 by rewrite a1El.
  rewrite (_ : a[p3, p1] l = a[p2, p1] l); last by rewrite lE1.
  apply: (@case2 _ IH) ⇒ //.
  - by rewrite (_ : a[p1, p3] _ = a[p1, p3] 1).
  - move⇒ k hK; rewrite {3}lE1 in hK.
    have → : k = inord 1.
      apply/val_eqP; rewrite /= inordK //.
      by case: (k : nat) hK ⇒ [] // [|].
    rewrite inordK //= !(apegS, apeg0) //= codom_subC.
    have := cH (inord 1).
    rewrite inordK // !(apegS, apeg0).
    by apply.
  - by rewrite KH2 lE1.
  move⇒ k.
  have [->|[->|->]] // : k = ord0 ∨ k = (inord 1) ∨ k = (inord 2).
  - move: k; rewrite lE1.
    case ⇒ [] []; first by left; apply: val_inj ⇒ /=.
    case.
      by right; left; apply: val_inj; rewrite /= inordK.
    case ⇒ //.
    by right; right; apply: val_inj; rewrite /= inordK.
  by rewrite -[in inord 1]aE1 uaLEp2 aE1 inordK.
  rewrite {1}(_ : inord 2 = ord_max); last first.
    by apply/val_eqP; rewrite /= lE1 inordK.
  by rewrite KH2 lE1 /= inordK.
pose u2r := [ffun i : 'I_(3 × c).-2.+1 ⇒ u2 (inord i.+2)].
pose pa1 := a[p1, p3] a1.
pose pa1S := a[p1, p3] a1.+1.
have cH8 (k : 'I_(3 × c).-2.+1) :
  0 < k < (3 × c).-2 → codom (u2r k) \subset [:: p2; a[pa1, pa1S] k].
  move⇒ /andP[k_gt0 k3L3a].
  have k2L3c : k.+2 < (3 × c).
    by have := k3L3a; rewrite -{2}subn2 ltn_subRL add2n.
  rewrite !ffunE inordK ?ltnS 1?ltnW //.
  case: eqP ⇒ [km3E0 /= |/eqP km3D0].
    have k3_gt0 : 0 < k.+2 %/ 3.
      case: (k: nat) k_gt0 km3E0 ⇒ // [] //= k1 _ _.
      by rewrite (divnMDl 1 k1 (_ : 0 < 3)).
    have a1k3Ll1 : a1 + k.+2 %/ 3 < l.+1.
      move: k2L3c.
      rewrite {1}(divn_eq k.+2 3) km3E0 addn0 mulnC ltn_mul2l /= ⇒ k2L3c.
      rewrite -(subnK (_ : a1 ≤ l.+1)) ?(leq_trans a1Ll) //.
      by rewrite addnC ltn_add2r -/c.
    rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first.
      by rewrite /pa1S !addnS !apegS -apegD addnC.
    rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + (k.+2) %/ 3)) ; last first.
      rewrite apegO oddD {1}(divn_eq k.+2 3) !oddD odd_mul andbT -oddD.
      by rewrite km3E0 addn0 -oddD -apegO.
    have /H : 0 < (inord (a1 + k.+2 %/ 3) : 'I_l.+2) < l.+1.
      rewrite inordK; first by rewrite addn_gt0 a1_gt0.
      by rewrite ltnS ltnW.
    by rewrite ffunE inordK // ltnS ltnW.
  case: eqP ⇒ [km3E1|/eqP km3D1].
    rewrite eqn_leq ltnNge /=.
    have a1La1k : a1 < a1 + k.+2 %/3.
      by rewrite -{1}(addn0 a1) ltn_add2l divn_gt0.
    have a1k3Ll : a1 + k.+2 %/ 3 < l.+1.
      move: (ltnW k2L3c).
      rewrite {1}(divn_eq k.+2 3) km3E1 addn1 mulnC ltn_mul2l /=.
      rewrite -(subnK (_ : a1 ≤ l.+1)) ?(leq_trans a1Ll) //.
      by rewrite addnC ltn_add2r -/c.
    rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first.
      by rewrite /pa1S !addnS !apegS -apegD addnC.
    rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + (k.+2) %/ 3).+1) ; last first.
      rewrite apegS apegO {1}(divn_eq k.+2 3) !oddD odd_mul andbT.
      by rewrite km3E1 addbT addbN -oddD -oddS -apegO apegS.
    case: (sitiHb (a1 + k.+2 %/ 3)) ⇒ // [| siH _ _]; first by rewrite a1La1k.
    by move: siH; rewrite a1Max // ltnS ltnW.
  have km3E2 : k.+2 %% 3 = 2.
    by case: (_ %% _) (ltn_mod k.+2 3) km3D0 km3D1 ⇒ // [] [|[|]].
  rewrite ifN; last by case: (k : nat) k_gt0.
  have a1La1k : a1 < a1 + k.+2 %/3.
    by rewrite -{1}(addn0 a1) ltn_add2l divn_gt0.
  have a1k3Ll : a1 + k.+2 %/ 3 < l.+1.
    have: k.+2 %/ 3 × 3 < 3 × c.
      rewrite ltnW //.
      move: (ltnW k2L3c).
      by rewrite {1}(divn_eq k.+2 3) km3E2 addn2.
    rewrite mulnC ltn_mul2l /=.
    rewrite -(subnK (_ : a1 ≤ l.+1)) ?(leq_trans a1Ll) //.
    by rewrite addnC ltn_add2r -/c.
  rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first.
    by rewrite !addnS /pa1S !apegS -apegD addnC.
  rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + (k.+2) %/ 3)) ; last first.
    rewrite apegO {1}(divn_eq k.+2 3) !oddD odd_mul andbT.
    by rewrite km3E2 addbF -oddD -apegO.
  rewrite codom_subC.
  case: (sitiHb (a1 + k.+2 %/ 3)) ⇒ // [| _ tiH _]; first by rewrite a1La1k.
  by move: tiH; rewrite a1Max // a1La1k ltnS ltnW.
have c_gt0 : 0 < c by rewrite ltnW.
have P8 :
  (S_[(3 × c).-2] n.+1).*2 ≤
  \sum_(i < (3 × c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove +
  sp ta1 (3 × c).-2 pa1 + sp ↓[u ord_max] (3 × c).-2 (a[p3, p1] l).
  apply: leq_trans (IH _ _ _ _ _ _ cH8) _; rewrite /pa1 /pa1S {cH8}//.
  - by rewrite apegS apeg_eqC.
  - by rewrite eq_sym.
  repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.
  - apply: eq_bigr ⇒ i _.
    by rewrite ![u2r _]ffunE !inordK // ltnS // ltnW.
  - apply: eq_bigr ⇒ i _; congr ((_ != _) × _).
    rewrite !ffunE /= !inordK //=.
    by rewrite (leq_trans (_ : 2 < (3 × 1).+1)) // ltnS leq_mul2l ltnW.
  apply: eq_bigr ⇒ i _; congr ((_ != _) × _).
    rewrite !ffunE /= !prednK ?muln_gt0 //=; last first.
      by rewrite -subn1 ltn_subRL addn0 (leq_trans (_ : _ < 3 × 1)) //
                 leq_mul2l.
    rewrite inordK // mod3E /= div3E addnC subnK; last first.
      by apply: (leq_trans a1Ll).
    by rewrite ffunE; congr (u _ _ ); apply/val_eqP; rewrite /= inordK.
  rewrite /pa1 /pa1S -[RHS]apegS -(subnK (_ : a1 ≤ l.+1)) // -/c.
    rewrite apegS -apegD apegO -subn2 oddD oddB //.
      by rewrite odd_mul /= addbF -oddD -apegO.
    by rewrite (leq_trans (_ : _ < 3 × 1)) // leq_mul2l //.
  by rewrite ltnW.
rewrite {cH8}//.
have l_gt0 : 0 < l.
  by rewrite -ltnS l1E aE1 add1n addSn ltnS addn_gt0 c_gt0 orbT.
have c3m2_gt1 : 1 < (3 × c).-2.
  by rewrite -subn2 ltn_subRL -[2 +1]/(3 × 1) ltn_mul2l.
have {}P8 := leq_trans P8 (leq_add (leq_add (leqnn _) (leqnn _))
                      (leq_sum_beta _ _)).
set y7S := sp _ _ _ in P8; set y8S := \sum_(_ < n.+1) _ in P8.
rewrite !sum_beta_S // KH1 KH2 !eqxx !addn0 -/y8S.
rewrite (_ : sd u =
  \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove +
  \sum_(a ≤ i < a1) `d[u (inord i), u (inord i.+1)]_smove +
  \sum_(a1 ≤ i < l.+1) `d[u (inord i), u (inord i.+1)]_smove); last first.
  rewrite /sd -[X in _ = X + _ + _](big_mkord xpredT
                (fun i ⇒ `d[u (inord i), u (inord i.+1)]_smove)).
  by rewrite -!big_cat_nat ?big_mkord //= ltnW.
rewrite -{}P1 -{}P2.
move: P3 ⇒ P3.
rewrite -2!addnA.
apply: leq_trans (leq_add (leq_add (leqnn _) P3) (leqnn _)); rewrite {P3}//.
have du2E : `d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove =
             \sum_(i < 2) `d[u2 (inord i), u2 (inord i.+1)]_smove.
  rewrite !big_ord_recr /= big_ord0 !ffunE !inordK //= ?addn0 //.
    by rewrite ltnW // ltnS (leq_mul2l 3 1).
  by rewrite ltnS muln_gt0.
rewrite (_ : sd u2 =
  (`d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove) +
  \sum_(i < (3 × c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove);
   last first.
  rewrite /sd du2E.
  rewrite -!(big_mkord xpredT
                (fun i ⇒ `d[u2 (inord i), u2 (inord i.+1)]_smove)).
  rewrite -!(big_mkord xpredT
                (fun i ⇒ `d[u2 (inord i.+2), u2 (inord i.+3)]_smove)).
  rewrite[X in _ = _ + X] (eq_bigr
                (fun i ⇒ `d[u2 (inord (i + 2)), u2 (inord (i + 2).+1)]_smove));
    last by move⇒ i_; rewrite !addn2.
  rewrite -subn2.
  have <- := big_addn _ _ _ xpredT
               (fun i ⇒ `d[u2 (inord i), u2 (inord i.+1)]_smove).
  rewrite -big_cat_nat //.
  by rewrite ltnW // (leq_mul2l 3 1).
set x3S := \sum_(_ < _) _ in P8; rewrite -/x3S.
have [|b_gt0] := leqP b 0; last first.
  have cH1 (k : 'I_(3 × a).+1) :
    0 < k < 3 × a → codom (u1 k) \subset [:: p3; a[p1, p2] k].
    move⇒ /andP[k_gt0 k_ltb].
    rewrite {2}aE1 muln1 in k_ltb.
    rewrite ffunE !modn_small // !divn_small // inord_eq0 //.
    rewrite [in 3 × a.-1]aE1 /=.
    case: (k : nat) k_gt0 k_ltb ⇒ //= [] [|[|]] //= _ _.
      rewrite apegS apeg0.
      by have := sam1C; rewrite /pa aE1.
    by rewrite codom_subC.
  set x0S := sd u1.
  have P4 :
    (S_[3 × a] n.+1).*2 ≤ x0S + sp ↓[u ord0] 3 p1 +
                                 sp ↓[u (inord a)] 3 p2.
    apply: leq_trans (IH _ _ _ _ _ _ cH1) (leq_add (leq_add _ _) _);
        rewrite // 1?eq_sym //.
      by apply: leq_sum ⇒ i _; rewrite ffunE /= inord_eq0 // aE1 muln1.
    by apply: leq_sum ⇒ i _; rewrite ffunE /= mod3E /= div3E // aE1 muln1.
  have {}P4 := leq_trans P4 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                        (leqnn _)).
  set y0S := \sum_(_ < _) _ in P4; set y1S := sp _ _ _ in P4.
  have [b_gt1|b_le2] := leqP 2 b.
    pose u3 := [ffun i ⇒ ↓[u (inord ((i : 'I_b.+1) + a))]].
    pose paS := a[p1, p3] a.+1.
    have cH6 (k : 'I_b.+1) :
        0 < k < b → codom (u3 k) \subset [:: p2; a[pa, paS] k].
      move⇒ /andP[k_gt0 kLb].
      have kBound : 0 < k + a < l.+1.
        rewrite (leq_trans a_gt0) ?leq_addl //=.
        move: kLb; rewrite /b ltn_subRL addnC ⇒ /leq_trans→ //.
        by rewrite ltnW.
      rewrite ffunE codom_liftr //.
      have := @cH (inord (k + a)).
      rewrite /pa /paS apegS -apegD /= !inordK //; last first.
        by rewrite ltnW // ltnS; case/andP: kBound.
      by apply.
    have {cH6}P6 :
    (S_[b] n.+1).*2 ≤ sd u3 + sp (u3 ord0) b pa +
                               sp (u3 ord_max) b (a[pa, paS] b).
      apply: IH cH6 ⇒ //; try by rewrite /pa /paS // eq_sym.
      by rewrite /paS apegS apeg_eqC.
    set x1S := \sum_(_ ≤ _ < _) _.
    rewrite !ffunE (_ : sd u3 = x1S) in P6; last first.
      rewrite /x1S -[a]add0n big_addn -/b big_mkord.
      by apply: eq_bigr ⇒ i _; rewrite !ffunE !inordK ?ltnS // ltnW.
    rewrite add0n subnK // in P6.
    set y2S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6.
    have aLl : a ≤ l by apply: leq_trans aLa1 _.
    have y1Sy2SE : y1S + y2S ≤ (S_[1] n).*2 + α_[maxn 3 b] n.
      apply: sum_alpha_diffE ⇒ //; first by rewrite /pa eq_sym.
      apply/codom_liftr.
      have /cH : 0 < (inord a : 'I_l.+2) < l.+1 by rewrite inordK // a_gt0.
      by rewrite inordK // aE1 /=.
    pose u5 := [ffun i : 'I_3 ⇒
                     if i == 0 :> nat then ↓[u (inord a1)]
                     else if i == 1 :> nat then sa1 else ta1].
    have cH7 (k : 'I_3) :
      0 < k < 2 → codom (u5 k) \subset [:: p1; a[p2, p3] k].
      move⇒ /andP[k_gt0 k_lt2].
      rewrite !ffunE.
      by have ->/= : k = 1 :> nat by case: (k : nat) k_gt0 k_lt2 ⇒ // [] [|].
    have P7 :
      (S_[2] n.+1).*2 ≤
      (`d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove) +
         sp ↓[u (inord a1)] 2 p2 + sp ta1 2 p2.
      apply: (leq_trans (IH _ _ _ _ _ _ cH7)) ⇒ //.
        by rewrite eq_sym.
      repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.
      - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /=.
      - by apply: eq_bigr ⇒ i _; rewrite !ffunE.
      by apply: eq_bigr ⇒ i _; rewrite !ffunE.
    set x2S := (`d[_, _]_ _ + `d[_, _]_ _); rewrite -/x2S in P7.
    set y4S := sp _ _ _ in P7; set y5S := sp _ _ _ in P7.
    have y3Sy4SE : y3S + y4S ≤ (S_[1] n).*2 + α_[maxn b 2] n.
      apply: sum_alpha_diffE ⇒ //.
        by rewrite /paS apegS -apegD apeg_neq // eq_sym.
      apply: codom_liftr; rewrite codom_subC.
      have /cH : 0 < (inord a1 : 'I_l.+2) < l.+1.
        by rewrite inordK ?a1_gt0 // ltnS (leq_trans a1Ll).
      rewrite inordK ?ltnS ?(leq_trans a1Ll) //.
      by rewrite /paS apegS -apegD subnK.
    rewrite (maxn_idPl _) // in y3Sy4SE.
    have y5Sy7SE : y5S + y7S ≤ (S_[1] n).*2 + α_[maxn 2 (3 × c).-2] n.
      by apply: sum_alpha_diffE ⇒ //; first by rewrite /pa1 eq_sym.
    rewrite (maxn_idPr _) // in y5Sy7SE.
    rewrite -/y0S.
    move: P4 P6 P7 P8 ⇒ P4 P6 P7 P8.
    rewrite -(leq_add2r y1S); applyr P4.
    rewrite -(leq_add2r (y2S + y3S)); applyr P6.
    rewrite -(leq_add2r (y4S + y5S)); applyr P7.
    rewrite -(leq_add2r y7S); applyr P8.
    applyl y5Sy7SE; applyl y3Sy4SE; applyl y1Sy2SE.
    rewrite aE1 !muln1.
    have F1 := dsum_alphaL_S (3 × c).-2 n.
    rewrite [X in _ ≤ _ + X]mul2n -addnn -ltnS ![in X in _ ≤ X]addnA
            -![in X in _ ≤ X]addnS {2}F1 {F1}//.
    gsimpl.
    have F2 i k : 0 < i → S_[i.-1] k.+1 ≤ S_[(3 ×i).-2] k + i.-1.
      move⇒ i_gt0; apply: leq_trans (dsum_alpha3l _ _) _.
      rewrite leq_add2r.
      apply: (increasingE (increasing_dsum_alphaL_l _)).
      by rewrite -{2}[i]prednK // mulnS addSn add2n /=.
    have F2n := F2 c n c_gt0.
    have F2n1 := F2 c n.+1 c_gt0.
    have F3 : c = c.-1.+1 by rewrite prednK.
    rewrite {}[in 2 × c]F3.
    gsimpl.
    applyr F2n; applyr F2n1; rewrite {F2}//.
    have l_gt1 : 1 < l.
      by rewrite -ltnS l1E aE1 add1n addSn ltnS (leq_trans b_gt1) // leq_addr.
    have F4 := SH l_gt1; applyl F4.
    have cB1_gt0 : 0 < c.-1 by rewrite -ltnS prednK.
    have F5 : S_[l.+1] n.+2 + S_[1] n.+2 ≤ S_[c.-1] n.+2 + S_[b.+3] n.+2.
      rewrite [X in _ ≤ X]addnC.
      rewrite (_ : l.+1 = 1 + c.-2 + b.+2); last first.
        by rewrite l1E aE1 !add1n -addSnnS !prednK // addnC.
      rewrite (_ : c.-1 = 1 + c.-2); last first.
         by rewrite add1n prednK // -ltnS prednK.
      by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).
    have F6 : S_[l] n.+1 + S_[1] n.+1 ≤ S_[c.-1] n.+1 + S_[b.+2] n.+1.
      rewrite [X in _ ≤ X]addnC.
      rewrite (_ : l = 1 + c.-2 + b.+1); last first.
        rewrite -[l]/(l.+1.-1) l1E aE1.
        by rewrite !add1n -addSnnS !prednK // addnC addnS.
      rewrite (_ : c.-1 = 1 + c.-2); last first.
         by rewrite add1n prednK // -ltnS prednK.
      by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).
    rewrite -(leq_add2r (S_[b.+2] n.+1)); applyr F6.
    rewrite -(leq_add2r (S_[b.+3] n.+2)); applyr F5; gsimpl.
    have [b_gt2|b_le3] := leqP 3 b.
      have F7 := dsum_alphaL_S b n; rewrite {}F7; gsimpl.
      have F8 : S_[b.+3] n.+2 ≤ S_[b.+2] n.+1 + (α_[1] n.+1).*2.
        by apply: dsum_alphaL_alpha.
      applyl F8.
      have F9 : S_[b.+1] n.+1 ≤ S_[b] n + (α_[1] n).*2.
        by apply: dsum_alphaL_alpha.
      rewrite -leq_double in F9.
      rewrite -(leq_add2r (4 × α_[1] n)); applyr F9.
      have F10 : S_[1] n.+1 + S_[b.+2] n.+1 ≤ S_[b.+1] n.+1 + S_[2] n.+1.
        rewrite addnC -[b.+2]/(1 + 1 + b).
        by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).
      rewrite -leq_double in F10; applyr F10.
      rewrite -2!ltnS [in X in _ ≤ X]mul2n -![in X in _ ≤ X]addSn -doubleS.
      have F11 := dsum_alpha3_S n.+1; rewrite -F11.
      have F12 := dsum_alphaL_S 1 n.+1; rewrite F12.
      have F13 := dsum_alphaL_S 1 n; rewrite !F13; gsimpl.
      by have F14 := alphaL_1_2 n; applyl F14; gsimpl.
    have bE2 : b = 2.
      by case: (b) b_gt1 b_le3 ⇒ // [] [|[|]].
    rewrite bE2.
    rewrite ![in X in _ ≤ X]mul2n -!addnn.
    have F1 := dsum_alphaL_S 2 n; rewrite {1}F1.
    have F2 := dsum_alphaL_S 3 n; rewrite {1}F2.
    have F3 : S_[5] n.+2 ≤ S_[4] n.+1 + (α_[1] n.+1).*2.
      by apply: dsum_alphaL_alpha.
    rewrite -[3 + 2]/5 -[2 + 2]/4; applyl F3.
    have F4 : S_[4] n.+1 ≤ S_[3] n + (α_[1] n).*2.
      by apply: dsum_alphaL_alpha.
    rewrite -leq_double in F4; applyl F4; gsimpl.
    rewrite -ltnS.
    have F5 := dsum_alpha3_S n.+1.
    rewrite -![in X in _ ≤ X]addSn -F5.
    have F6 := dsum_alpha3_S n.
    rewrite addnAC -!addnS -F6.
    rewrite -leq_double.
    have F7 := leq_dsum_alpha_2l_1 n.+1.
    have F8 := leq_dsum_alpha_2l_1 n.
    rewrite -[_ ≤ _]orFb -(leq_mul2l 3) in F7.
    applyr F7; applyr F8; gsimpl.
    have F9 := dsum_alphaL_S 1 n.+1.
    have F10 := dsum_alphaL_S 1 n.
    rewrite !(F9, F10); gsimpl.
    by have F11 := alphaL_1_2 n; applyl F11; gsimpl.
  have bE1 : b = 1.
    by case: (b) b_gt0 b_le2 ⇒ // [] [|].
  have a1E2 : a1 = 2.
    by move: bE1; rewrite /b aE1; case: (a1) ⇒ // [] [|[]].
  pose u3 :=
    [ffun i : 'I_4 ⇒
    if i == 0 :> nat then ↓[u (inord a)] else
    if i == 1 :> nat then ↓[u (inord a1)] else
    if i == 2 :> nat then sa1 else ta1].
  set x1S := \sum_(_ ≤ _ < _) _.
  set d1 := `d[_, _]_ _ + `d[_, _]_ _.
  rewrite -/y0S.
  changer (a.*2 + x0S + c.*2 + x3S + y0S + y8S + (x1S + d1)).
  have → : x1S + d1 = \sum_(i < 3) `d[u3 (inord i), u3 (inord i.+1)]_smove.
    rewrite /x1S aE1 a1E2 big_nat1 /d1 !big_ord_recr big_ord0 /=.
    by rewrite !ffunE !inordK //= aE1 a1E2 add0n !addnA.
    have l_gt2 : 2 < l by rewrite -ltnS l1E aE1 bE1 !add1n.
  set x6S := \sum_(_ < 3) _.
  have cH6 (k : 'I_4) :
    0 < k < 3 → codom (u3 k) \subset [:: pa1; a[pa1S, p2] k].
    move⇒ /andP[k_gt0 k_lt3].
    rewrite !ffunE eqn_leq leqNgt k_gt0 /=.
    case: eqP ⇒ [->/=|/eqP kD1].
      apply: codom_liftr; rewrite codom_subC.
      have /cH : 0 < (inord a1 : 'I_l.+2 ) < l.+1.
        by rewrite inordK a1E2 // (leq_trans l_gt2).
      by rewrite inordK // a1E2 (leq_trans l_gt2) // ltnW.
    have → : k = 2 :> nat.
      by case: (k : nat) k_gt0 k_lt3 kD1 ⇒ // [] [|[]].
    by have := sa1C; rewrite eqxx /pa1 /pa1S !(apegS, apeg0) codom_apeg.
  have P6 :
    (S_[3] n.+1).*2 ≤ x6S + sp (u3 ord0) 3 pa1S + sp (u3 ord_max) 3 p2.
    apply: IH cH6; rewrite /pa1S /pa1 //.
    by rewrite a1E2 eq_sym.
  rewrite !ffunE /= in P6.
  set y2S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6.
  have y1Sy2SE : y1S + y2S ≤ (S_[1] n).*2 + α_[3] n.
    apply: sum_alpha_diffE ⇒ //; first by rewrite eq_sym /pa1S a1E2.
    have /H : 0 < (inord a : 'I_l.+2) < l.+1; first by rewrite inordK // aE1.
    by rewrite ffunE inordK // /pa1S /= aE1 a1E2.
  have lEc : l = c.+1 by rewrite -[l]/l.+1.-1 l1E aE1 bE1.
  rewrite lEc.
  have y3Sy7SE : y3S + y7S ≤ (S_[1] n).*2 + α_[maxn 3 (3 × c).-2] n.
    by apply: sum_alpha_diffE ⇒ //; first by rewrite /pa1 a1E2 eq_sym.
  rewrite (maxn_idPr _) in y3Sy7SE; last first.
    by rewrite -subn2 ltn_subRL ltnW // (leq_mul2l 3 2).
  move: P4 P6 P8 ⇒ P4 P6 P8.
  rewrite -(leq_add2r y1S); applyr P4.
  rewrite -(leq_add2r (y2S + y3S)); applyr P6.
  rewrite -(leq_add2r y7S); applyr P8.
  rewrite aE1 !muln1.
  applyl y1Sy2SE; applyl y3Sy7SE.
  rewrite ![in X in _ ≤ X]mul2n -!addnn.
  have F1 := dsum_alphaL_S 3 n; rewrite {1}F1.
  have F2 := dsum_alphaL_S (3 × c).-2 n; rewrite {1}F2; gsimpl.
  have F4 k : S_[c.-1] k.+1 ≤ S_[(3 ×c).-2] k + c.-1.
    apply: leq_trans (dsum_alpha3l _ _) _.
    rewrite leq_add2r.
    apply: (increasingE (increasing_dsum_alphaL_l _)).
    by rewrite -{2}[c]prednK // mulnS addSn add2n /=.
  have F4n := F4 n.
  have F4n1 := F4 n.+1.
  have F5 := prednK c_gt0.
  rewrite -{}[in 2 × c]F5.
  applyr F4n1; applyr F4n.
  have l_gt1 : 1 < l by rewrite lEc.
  have F6 : (S_[c.+2] n.+2).*2 ≤
             S_[c.+2] n.+2 + S_[c.+1] n.+1 + (α_[1] n.+1).*2.
    by have := (SH l_gt1); rewrite lEc.
  applyl F6.
  have F7 : S_[c.+2] n.+2 + S_[1] n.+2 ≤ S_[c.-1] n.+2 + S_[4] n.+2.
    rewrite (_ : c.+2 = 1 + 3 + c.-2); last first.
      by rewrite !addSn add0n !prednK ?addn2 // -ltnS prednK.
    rewrite {2}(_ : c.-1 = 1 + c.-2); last first.
      by rewrite add1n prednK // -ltnS prednK.
    by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).
  have F8 : S_[c.+1] n.+1 + S_[1] n.+1 ≤ S_[c.-1] n.+1 + S_[3] n.+1.
    rewrite (_ : c.+1 = 1 + 2 + c.-2); last first.
      by rewrite !addSn add0n !prednK ?addn2 // -ltnS prednK.
    rewrite {2}(_ : c.-1 = 1 + c.-2); last first.
      by rewrite add1n prednK // -ltnS prednK.
    by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).
  rewrite -(leq_add2r (S_[1] n.+2 + S_[1] n.+1)); applyl F7; applyl F8; gsimpl.
  have F9 : S_[4] n.+2 ≤ S_[3] n.+1 + (α_[1] n.+1).*2.
    by apply: dsum_alphaL_alpha.
  applyl F9.
  have F10 := dsum_alpha3_S n.
  have F11 := dsum_alpha3_S n.+1.
  gsimpl.
  rewrite -ltnS -![in X in _ ≤ X]addSn -{}F11.
  rewrite -ltnS -3![in X in _ ≤ X]addSn -[in X in _ ≤ X]addnS -{}F10.
  have F12 := dsum_alphaL_S 1 n.+1.
  have F13 := dsum_alphaL_S 1 n.
  rewrite F12 F13; gsimpl.
  have F14 := alphaL_1_2 n; rewrite -leq_double in F14.
  by applyl F14; gsimpl.
rewrite leqn0 ⇒ /eqP bE0.
have a1Ea : a1 = a by rewrite -(subnK aLa1) -/b bE0.
rewrite big_geq ?a1Ea // addn0.
have lEc : l = c by rewrite -[l]/(l.+1.-1) l1E aE1 bE0.
rewrite {1}lEc.
set d1 := `d[_, _]_ _ + `d[_, _]_ _.
set x0S := sd _; set y0S := \sum_(_ < _) _.
changer (a.*2 + c.*2 + x3S + y0S + y8S + (x0S + d1)).
pose u3 := [ffun i : 'I_6 ⇒
  if i == 0 :> nat then ↓[u ord0] else
  if i == 1 :> nat then sam1 else
  if i == 2 :> nat then tam1 else
  if i == 3 :> nat then ↓[u (inord a1)] else
  if i == 4 :> nat then sa1 else
  ta1].
have → : x0S + d1 = sd u3.
  rewrite /x0S /d1 /sd.
  rewrite -(big_mkord xpredT (fun i ⇒ `d[u1 (inord i), u1 (inord i.+1)]_ _)).
  rewrite {1}aE1 !(big_nat1, big_nat_recr) // !big_ord_recr big_ord0
          /= ?inordK //= !ffunE ?inordK ?a1Ea ?aE1 //=.
  by rewrite add0n !addnA inord_eq0.
have cH4 (k : 'I_6) :
    0 < k < 5 → codom (u3 k) \subset [:: p3; a[p1, p2] k].
    case: k ⇒ [] [|[|[|[|[]]]]] //= iH _; rewrite !ffunE !(apegS, apeg0).
  - by have := sam1C; rewrite /pa aE1.
  - by rewrite codom_subC.
  - rewrite a1Ea aE1.
  - have /H : 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite !inordK.
    by rewrite ffunE inordK // codom_subC.
  by rewrite codom_subC.
have P4 :
  (S_[5] n.+1).*2 ≤ sd u3 + sp ↓[u ord0] 5 p1 + sp ta1 5 p2.
  apply: leq_trans (IH _ _ _ _ _ _ cH4) _ ⇒ //; first by rewrite eq_sym.
  by apply: leq_add; rewrite !ffunE.
have {}P4 := leq_trans P4
  (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leqnn _)).
rewrite -/y0S in P4; set y1S := sp _ _ _ in P4.
set x1S := sd _ in P4; rewrite -/x1S.
have y1Sy7SE : y1S + y7S ≤ (S_[1] n).*2 + α_[maxn 5 (3 × c).-2] n.
  apply: sum_alpha_diffE ⇒ //; first by rewrite /pa1 eq_sym.
move: P4 P8 ⇒ P4 P8.
rewrite -(leq_add2r y1S); applyr P4.
rewrite -(leq_add2r y7S); applyr P8.
rewrite aE1 muln1.
applyl y1Sy7SE.
have leq_S5 k : 2 × S_[1] k.+1 + S_[1] k.+2 ≤ 3 × S_[5] k + 6.
  have F8 : S_[3] k + 2 × S_[6] k ≤ 3 × S_[5] k.
    rewrite -(leq_add2r (S_[4] k)).
    changel (S_[6] k + S_[3] k + (S_[6] k + S_[4] k)).
    changer (S_[4] k + S_[5] k + (S_[5] k + S_[5] k)).
    apply: leq_add.
      by apply: concaveEk1 3 2 1 (concave_dsum_alphaL_l _).
    by apply: concaveEk1 4 1 1 (concave_dsum_alphaL_l _).
  apply: leq_trans (leq_add F8 (leqnn _)).
  have F3k : S_[1] k.+1 ≤ S_[3] k + 1 by apply: dsum_alpha3l.
  have F3k1 : S_[2] k.+1 ≤ S_[6] k + 2 by apply: dsum_alpha3l.
  rewrite -leq_double in F3k1; applyr F3k1; applyr F3k; gsimpl.
  have F3k2 := leq_dsum_alpha_2l_1 k.+1.
  by applyr F3k2.
have [c_gt2|c_lt3] := leqP 3 c.
  rewrite (maxn_idPr _); last by rewrite -subn2 ltn_subRL (ltn_mul2l 3 2).
  have F1 k : S_[c.-1] k.+1 ≤ S_[(3 ×c).-2] k + c.-1.
    apply: leq_trans (dsum_alpha3l _ _) _.
    rewrite leq_add2r.
    apply: (increasingE (increasing_dsum_alphaL_l _)).
    by rewrite -{2}[c]prednK // mulnS addSn add2n /=.
  have F1n := F1 n.
  have F1n1 := F1 n.+1.
  have F2 := dsum_alphaL_S (3 × c).-2 n.
  rewrite [X in _ ≤ _ + X]mul2n -addnn {1}F2; gsimpl.
  have F3 : 2 × c = 2 + c.-1 + c.-1.
    by rewrite mul2n add2n prednK // addSnnS prednK // addnn.
  rewrite {}F3.
  applyr F1n; applyr F1n1.
  have F4 : S_[c.+1] n.+2 ≤ S_[c] n.+1 + (α_[1] n.+1).*2.
    by apply: dsum_alphaL_alpha.
  applyl F4.
  have F7n1 : S_[2] n.+2 + S_[c.+1] n.+2 ≤ S_[c.-1] n.+2 + S_[4] n.+2.
    rewrite addnC (_ : c.+1 = 2 + 2 + c.-2.-1); last first.
       by rewrite !addSn add0n !prednK // -ltnS prednK // -subn1 ltn_subRL //.
    rewrite {2}(_ : c.-1 = 2 + c.-1.-2); last first.
      by rewrite !addSn add0n !prednK // -?subn2 -?subn1 ltn_subRL.
    by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).
  have F7n : S_[2] n.+1 + S_[c] n.+1 ≤ S_[c.-1] n.+1 + S_[3] n.+1.
    rewrite addnC {1}(_ : c = 2 + 1 + c.-1.-2); last first.
      by rewrite !addSn add0n !prednK // -2!ltnS !prednK // -ltnS prednK.
    rewrite {2}(_ : c.-1 = 2 + c.-1.-2); last first.
      by rewrite !addSn add0n !prednK // -?subn2 -?subn1 ltn_subRL.
    by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).
  rewrite -(leq_add2l (S_[2] n.+2 + S_[2] n.+1)); applyl F7n1; applyl F7n.
  gsimpl.
  have F8 := leq_S5 n.+1.
  have F9 : S_[4] n.+2 ≤ S_[3] n.+1 + (α_[1] n.+1).*2.
    by apply: dsum_alphaL_alpha.
  applyl F9.
  rewrite -[_ ≤ _](leq_mul2l 3).
  rewrite -leq_double in F8; applyr F8.
  have F10 := dsum_alpha3_S n.+1.
  rewrite -(leq_add2r 6).
  changel (12 × (α_[1] n.+1) + 6 × (S_[1] n) + 6 × (S_[3] n.+1).+1).
  rewrite -F10.
  rewrite -leq_double.
  have F11 := leq_dsum_alpha_2l_1 n.+2.
  rewrite -[_ ≤ _](leq_mul2l 3) in F11.
  have F12 := leq_dsum_alpha_2l_1 n.+1.
  rewrite -[_ ≤ _](leq_mul2l 3) in F12.
  applyr F11; applyr F12; gsimpl.
  have F13 := dsum_alphaL_S 1 n.+2.
  have F14 := dsum_alphaL_S 1 n.+1.
  have F15 := dsum_alphaL_S 1 n.
  rewrite !(F13, F14, F15); gsimpl.
  have F16 := increasing_alphaL 1 n.+1.
  rewrite -[15]/(7 + 8) mulnDl [X in _ ≤ X]addnAC [X in _ ≤ X]addnC leq_add //.
    by rewrite leq_mul2l.
  case: (n) ⇒ [|[|[|[|n1]]]]; rewrite ?alpha_small //.
  have F17 : 3 × α_[1] n1.+1.+4 ≤ 4 × α_[1] n1.+4.
    by rewrite alpha_4_3.
  rewrite -[_ ≤ _]orFb -(leq_mul2l 8) mulnA in F17.
  rewrite -[_ ≤ _](leq_mul2l 3) mulnA.
  by apply: leq_trans F17 _; gsimpl.
have cE2 : c = 2 by case: (c) c_gt1 c_lt3 ⇒ [|[|[|]]].
rewrite cE2 (maxn_idPl _) // add1n -[2 × 2]/4 -[(3 × 2).-2]/4 -[2 + 4]/6.
rewrite [in X in _ ≤ X]mul2n -addnn.
have F1 := dsum_alphaL_S 5 n; rewrite {1}F1.
have F2 := dsum_alpha3_S n.+2.
rewrite -2!ltnS mul2n -![in X in X ≤ _]addSn -doubleS -{}F2.
have F3 := leq_S5 n.
have F4 := leq_S5 n.+1.
rewrite -[_ ≤ _](leq_mul2l 3); gsimpl.
applyr F3; applyr F4.
have F5 := leq_S4 n.+1; applyr F5.
have F6 := dsum_alphaL_S 1 n.+2.
have F7 := dsum_alphaL_S 1 n.+1.
have F8 := dsum_alphaL_S 1 n.
rewrite !(F6, F7, F8); gsimpl.
have F10 := alphaL_1_2 n.+1.
rewrite -[_ ≤ _]orFb -(leq_mul2l 4) in F10.
applyl F10; gsimpl.
case: (n) ⇒ [|[|[|[|n1]]]]; rewrite ?alpha_small //.
have F9 : 3 × α_[1] n1.+1.+4 ≤ 4 × α_[1] n1.+4.
  by rewrite alpha_4_3.
rewrite -[_ ≤ _]orFb -(leq_mul2l 4) in F9.
rewrite -[_ ≤ _](leq_mul2l 3).
by rewrite add1n; applyl F9; gsimpl.
Qed.

End Case3.

Lemma main p1 p2 p3 n l (u : {ffun 'I_l.+1 → configuration 4 n}) :
   p1 != p2 → p1 != p3 → p2 != p3 →
   p1 != p0 → p2 != p0 → p3 != p0 →
  (∀ k : 'I_l.+1, 0 < k < l →
                       codom (u k) \subset [:: p2; a[p1, p3] k]) →
  (S_[l] n).*2 ≤ \sum_(i < l) `d[u (inord i), u (inord i.+1)]_smove +
                    \sum_(k < n) (u ord0 k != p1) × β_[n, l] k +
                    \sum_(k < n) (u ord_max k != a[p1, p3] l) × β_[n, l] k.
Proof.
elim: n l p1 p2 p3 u ⇒ [|[|n] IH] l p1 p2 p3
                u p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0 cH.
- by rewrite /dsum_alphaL /conv /= dsum_alpha_0 muln0.
- rewrite /dsum_alphaL /conv /= dsum_alpha_1 dsum_alpha_0
          muln0 addn0 add0n muln1.
  rewrite [X in _ ≤ _ + X + _]big_ord_recl big_ord0 /= addn0.
  rewrite [X in _ ≤ _ + X]big_ord_recl big_ord0 /= addn0.
  have d0fE (c1 c2 : configuration 4 1) :
    c1 != `c[p0] → c2 != `c[p0] → `d[c1, c2]_smove = (c1 != c2).*2.
    move⇒ c1Dp0 c2Dp0.
    case: (gpath_connect (shanoi_connect c1 c2))
              ⇒ [] [/gpath_dist H |a [|b p]].
    - by rewrite H; move/eqP: H; rewrite gdist_eq0 ⇒ →.
    - case/gpathP; rewrite /= andbT ⇒ /moveP[z].
      rewrite [z]disk1_all ⇒ [] [zH _ _ _] aE.
      case/andP: zH ⇒ _; rewrite aE.
      move: c1Dp0 c2Dp0; rewrite !configuration1_eq !Ival_eq /= !ffunE /=.
      by do 2 case: val.
    move⇒ /gpath_dist; case: eqP ⇒ [<-|/eqP c1Dc2]; first by rewrite gdist0.
    move⇒ H; apply/eqP; rewrite eqn_leq {2}H /= andbT.
    have pH : path smove c1 [::`c[p0]; c2].
      rewrite /=; apply/and3P; split ⇒ //.
        apply/moveP; ∃ ord0; split ⇒ //=.
        - rewrite !ffunE; apply/andP; split; last by rewrite muln0.
          by move: c1Dp0; rewrite configuration1_eq ffunE.
        - by move⇒ i; rewrite [i]disk1_all.
        - by apply/on_topP ⇒ j; rewrite [j]disk1_all.
        by apply/on_topP ⇒ j; rewrite [j]disk1_all.
      apply/moveP; ∃ ord0; split ⇒ //=.
      - rewrite !ffunE; apply/andP; split⇒ //.
        by move: c2Dp0; rewrite configuration1_eq ffunE eq_sym.
      - by move⇒ i; rewrite [i]disk1_all.
      - by apply/on_topP ⇒ j; rewrite [j]disk1_all.
      by apply/on_topP ⇒ j; rewrite [j]disk1_all.
    rewrite -[1.*2]/(size [:: `c[p0]; c2]).
    by apply: gdist_path_le pH _.
  case: l u cH ⇒ [|l] u cH; first by rewrite (minn_idPr _).
  case: l u cH ⇒ [|l] u cH.
    rewrite (minn_idPr _) //.
    rewrite big_ord_recl big_ord0 addn0.
    rewrite inord_eq0 // (_ : inord 1 = ord_max); last first.
      by apply/val_eqP; rewrite /= inordK.
    rewrite /beta !(apegS, apeg0) /= alphaL1E -[_ 0]/1;
        do 2 case: eqP; rewrite /= ?addn0;
        try by move⇒ *; rewrite leq_addl.
    move⇒ u1E u0E.
    rewrite d0fE //.
    - by rewrite configuration1_eq u1E u0E p1Dp3.
    - by rewrite configuration1_eq ffunE u0E.
    by rewrite configuration1_eq ffunE u1E.
  rewrite (minn_idPl _) // -[_.*2]/4.
  rewrite big_ord_recl big_ord_recr /=.
  rewrite -!addnA addnC -!addnA (leq_trans _ (leq_addl _ _)) //.
  rewrite !apegS /beta /= alphaL_0 (minn_idPl _) /bump /= ?add1n //.
  rewrite addnCA addnC !addnA -addnA -[4]/(2 + 2).
  apply: leq_add.
    case: eqP ⇒ /= [umE|umD]; last by rewrite leq_addl.
    rewrite addn0 d0fE.
    - case: eqP ⇒ // H.
      have /cH : 0 < (inord l.+1 : 'I_l.+3) < l.+2 by rewrite inordK /=.
      move⇒ /subsetP/(_ _ (codom_f _ sdisk)).
      rewrite H (_ : inord l.+2 = ord_max).
        rewrite umE inordK // apegS //= !inE.
        rewrite (apeg_eqC _ _ _) // (negPf (apeg_neq _ _ _)) //=.
          by rewrite (negPf p1Dp3).
        by rewrite eq_sym.
      by apply/val_eqP; rewrite /= inordK.
    - rewrite configuration1_eq ffunE.
      case: (_ =P _) ⇒ // H.
      have /cH : 0 < (inord l.+1 : 'I_l.+3) < l.+2 by rewrite inordK /=.
      move⇒ /subsetP/(_ _ (codom_f _ sdisk)).
      by rewrite H !inE eq_sym (negPf p2Dp0) /= eq_sym (negPf (apeg_neq _ _ _)).
    rewrite configuration1_eq ffunE.
    rewrite (_ : inord l.+2 = ord_max).
      by rewrite umE apeg_neq.
    by apply/val_eqP; rewrite /= inordK.
  case: eqP ⇒ /= [u0E|u0D]; last by rewrite leq_addl.
  rewrite addn0 d0fE.
  - case: eqP ⇒ // H.
    have /cH : 0 < (inord 1 : 'I_l.+3) < l.+2 by rewrite inordK /=.
    move⇒ /subsetP/(_ _ (codom_f _ sdisk)).
    rewrite -H inord_eq0 // u0E inordK //= !(apegS, apeg0).
    by rewrite !inE (negPf p1Dp2) (negPf p1Dp3).
  - by rewrite configuration1_eq ffunE inord_eq0 // u0E.
  rewrite configuration1_eq ffunE.
  case: eqP ⇒ // H.
  have /cH : 0 < (inord 1 : 'I_l.+3) < l.+2 by rewrite inordK /=.
  move⇒ /subsetP/(_ _ (codom_f _ sdisk)).
  by rewrite H !inE eq_sym (negPf p2Dp0) /= eq_sym (negPf (apeg_neq _ _ _)).
case: l u cH ⇒ [|l] u cH; first by rewrite S0E.
rewrite apegS.
pose u' : {ffun 'I_l.+2 → configuration 4 n.+1} :=
     [ffun i : 'I_l.+2 ⇒ ↓[u i]].
have H (k : 'I_l.+2) :
  0 < k < l.+1 → codom (u' k) \subset [:: p2; a[p1, p3] k].
  by move⇒ k1; rewrite ffunE; apply/codom_liftr/cH.
pose K := (u ord0 ord_max != p1) +
          (u ord_max ord_max != a[p3, p1] l).
have [HK|] := boolP ((K == 2) || ((K == 1) && (l == 0))).
  rewrite dsum_alphaL_S doubleD.
  have IH' := IH _ p1 p2 p3 u'
              p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0 H.
  rewrite apegS in IH'.
  rewrite ![\sum_(_ < _.+2) _]big_ord_recr /=.
  set u1 := \sum_ (_ < _) _; set u2 := \sum_ (_ < _) _; set u3 := \sum_ (_ < _) _.
  rewrite -!addnA [_ + (u3 + _)]addnCA 2!addnA.
  apply: leq_add.
    apply: leq_trans IH' _.
    apply: leq_add; last first.
      apply: leq_sum ⇒ i _.
      apply: leq_mul.
        rewrite leq_eqVlt; apply/orP; left; apply/eqP.
        by rewrite !ffunE; congr (u _ _ != _); apply/val_eqP.
      rewrite {2}/beta eqn_leq [_ ≤ i]leqNgt ltn_ord !andbF /=.
    apply: geq_beta.
    apply: leq_add; last first.
      apply: leq_sum ⇒ i _.
      apply: leq_mul.
        rewrite leq_eqVlt; apply/orP; left; apply/eqP.
        by rewrite !ffunE; congr (u _ _ != _); apply/val_eqP.
      rewrite {2}/beta eqn_leq [_ ≤ i]leqNgt ltn_ord !andbF /=.
      apply: geq_beta.
    apply: leq_sum ⇒ i _.
    rewrite !ffunE.
    by apply/gdist_cunlift/shanoi_connect.
  rewrite -mulnDl -/K.
  case/orP: HK ⇒ [/eqP->|/andP[/eqP→ /eqP->]].
    by rewrite mul2n leq_double leq_beta.
  by rewrite mul1n /beta /= /alphaL /delta !S1E.
rewrite negb_or negb_and.
have: K ≤ 2 by rewrite /K; do 2 case: (_ != _).
case: ltngtP; rewrite // ltnS.
case: ltngtP ⇒ //= KE _ _ l_gt0; last first.
  move: KE; rewrite /K.
  (case: eqP ⇒ [KH1|/eqP KH1] /=; case: eqP) ⇒ // [/eqP KH2|KH2] _.
    by apply: (@case1 _ IH) cH KH1 KH2 l_gt0.
  pose u1 : {ffun 'I_l.+2 → configuration 4 n.+2} :=
     [ffun i : 'I_l.+2 ⇒ u (inord (l.+1 - i))].
  have → : \sum_(i < l.+1) `d[u (inord i), u (inord i.+1)]_smove =
            \sum_(i < l.+1) `d[u1 (inord i), u1 (inord i.+1)]_smove.
    have F : injective (fun i : 'I_l.+1 ⇒ (inord (l - i) : 'I_l.+1)).
      move⇒ i j /val_eqP.
      have lBiLl (i1 : 'I_l.+1) : l - i1 < l.+1.
        by rewrite ltn_subLR ?leq_addl // -ltnS.
      rewrite /= !inordK // ⇒ /eqP liE; apply/val_eqP ⇒ /=.
      rewrite -(subKn (_ : i ≤ l)); last by rewrite -ltnS.
      by rewrite liE subKn // -ltnS.
    rewrite (reindex_inj F) /=.
    apply: eq_bigr ⇒ i _; rewrite !ffunE.
    have iLl2 : i < l.+2 by apply: leq_trans (ltn_ord _) _.
    have lBiLl : l - i < l.+1 by rewrite ltn_subLR ?leq_addl // -ltnS.
    have iLl : i ≤ l by rewrite -ltnS.
    rewrite gdistC; last by apply/move_sym/ssym.
    congr (`d[u _,u _]_smove).
      by apply/val_eqP; rewrite /= !inordK ?subSn.
    by apply/val_eqP; rewrite /= !inordK // ?subSS ltnS // ltnW.
  pose p1' := a[p3, p1] l.
  pose p3' := a[p1, p3] l.
  have → : \sum_(k < n.+2) (u ord0 k != p1) × β_[n.+2, l.+1] k =
            \sum_(k < n.+2) (u1 ord_max k != a[p1', p3'] l.+1) ×
                            β_[n.+2, l.+1] k.
    apply: eq_bigr ⇒ i _; congr (_ × _).
    rewrite ffunE subnn.
    by rewrite inord_eq0 // -apegD addSn addnn apegS apeg_double.
  have → : \sum_(k < n.+2)
              (u ord_max k != a[p3, p1] l) × β_[n.+2, l.+1] k =
            \sum_(k < n.+2) (u1 ord0 k != p1') × β_[n.+2, l.+1] k.
    apply: eq_bigr ⇒ i _; congr (_ × _).
    rewrite ffunE subn0.
    suff → : inord l.+1 = ord_max :> 'I_l.+2 by [].
    by apply/val_eqP; rewrite /= inordK.
  have cH1 (k : 'I_l.+2) :
     0 < k < l.+1 → codom (u1 k) \subset [:: p2; a[p1', p3'] k].
    move⇒ /andP[kH1 kH2]; rewrite ffunE.
    have F1 : k ≤ l.+1 by apply: ltnW.
    have F2 : l.+1 - k < l.+2.
      by rewrite ltn_subLR // addnS ltnS leq_addl.
    have → : a[p1', p3'] k = a[p1, p3] (inord (l.+1 - k) : 'I_l.+2).
      rewrite -apegD inordK // [RHS]apegO oddB //.
      by rewrite -oddD -apegO addSn apegS addnC.
    apply: cH; rewrite inordK // subn_gt0 // ltn_subLR // kH2 //=.
    by rewrite addnS ltnS -{1}[l.+1]add1n leq_add2r.
  rewrite -addnA [X in _ ≤ _ + X]addnC addnA apegS.
  apply: (@case1 _ IH) cH1 _ _ _ ⇒ //.
  - by rewrite apeg_neq // eq_sym.
  - by rewrite apeg_eqC // eq_sym.
  - by rewrite eq_sym apeg_neq // eq_sym.
  - by rewrite apeg_neq // eq_sym.
  - by rewrite apeg_neq // eq_sym.
  - rewrite ffunE subn0.
    suff → : inord l.+1 = ord_max :> 'I_l.+2 by [].
    by apply/val_eqP; rewrite /= inordK.
  by rewrite ffunE subnn inord_eq0 // -apegD addnn apeg_double.
move: KE; rewrite /K; do 2 case: eqP ⇒ //=.
move ⇒ uME u0E _.
by apply: (case3 IH _ _ _ _ _ _ cH).
Qed.

Lemma main_cor p1 p2 n :
  p1 != p0 → p2 != p0 → p1 != p2 →
  (S_[1] n).*2 ≤ `d[`c[p1, n],`c[p2, n]]_smove.
Proof.
move⇒ p1Dp0 p2Dp0 p1Dp2.
rewrite eq_sym in p2Dp0.
have [p3 [[p3Dp2 p3Dp0 p3Dp1] _]] := peg4comp3 p1Dp0 p1Dp2 p2Dp0.
rewrite eq_sym in p2Dp0.
pose u := [ffun i : 'I_2 ⇒ if i == 0 :> nat then
                             `c[p1, n] else `c[p2, n]].
suff :
  (S_[1] n).*2 ≤
  \sum_(i < 1) `d[u (inord i), u (inord i.+1)]_smove +
  \sum_(k < n) (u ord0 k != p1) × β_[n, 1] k +
  \sum_(k < n) (u ord_max k != p2) × β_[n, 1] k.
  rewrite big_ord_recr big_ord0 !ffunE /= inord_eq0 //= add0n.
  rewrite inordK //=.
  rewrite (eq_bigr (fun i : 'I_n ⇒ 0)) ⇒ [|i _]; last first.
    by rewrite !ffunE eqxx.
  rewrite -(big_mkord xpredT (fun⇒ 0)) sum_nat_const_nat muln0.
  rewrite (eq_bigr (fun i : 'I_n ⇒ 0)) ⇒ [|i _]; last first.
    by rewrite !ffunE eqxx.
  rewrite -(big_mkord xpredT (fun⇒ 0)) sum_nat_const_nat muln0.
  by rewrite !addn0.
apply: (@main p1 p3 p2) ⇒ //.
  by rewrite eq_sym.
by case⇒ [] [].
Qed.

Lemma gdist_shanoi4 (n : nat) (p1 p2 : peg 4) :
  p1 != p2 → p1 != p0 → p2 != p0 →
  `d[`c[p1, n], `c[p2, n]]_smove = (S_[1] n).*2.
Proof.
move⇒ p1Dp2 p1Dp0 p2Dp0; apply/eqP; rewrite eqn_leq.
by rewrite leq_shanoi4 // main_cor.
Qed.

End sHanoi4.